Parent Directory





.ispell_english

3124

20 years 
nogin 
Spelling changes.
For best results, upgrade to http://www.cs.cornell.edu/nogin/R…

Makefile

3566

19 years 
xiny 
Updated to reflect new file names.

czf_all.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_and.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_equal.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_exists.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_false.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_implies.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_itt_abel_group.ml

3555

19 years 
xiny 
Updated the definition and rules for abelian groups due to the adding
of "eqG".
…

czf_itt_abel_group.mli

3555

19 years 
xiny 
Updated the definition and rules for abelian groups due to the adding
of "eqG".
…

czf_itt_abel_group.prla

3555

19 years 
xiny 
Updated the definition and rules for abelian groups due to the adding
of "eqG".
…

czf_itt_all.ml

3281

20 years 
nogin 
The redundant "_resource" suffix should not be used in resource names.

czf_itt_all.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_all.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_and.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_and.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_and.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_axioms.ml

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_axioms.mli

3052

20 years 
jyh 
Two changes.
1. expand () now does sloppy expansion, so that proofs
can…

czf_itt_axioms.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_bool.ml

3380

19 years 
xiny 
Definitions for set difference & Boolean set

czf_itt_bool.mli

3380

19 years 
xiny 
Definitions for set difference & Boolean set

czf_itt_bool.prla

3380

19 years 
xiny 
Definitions for set difference & Boolean set

czf_itt_comment.ml

3329

20 years 
nogin 
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theor…

czf_itt_comment.mli

3223

20 years 
nogin 
Finally, I am able to commit what I was getting to
in all these commits over the…

czf_itt_comment.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_cyclic_group.ml

3558

19 years 
xiny 
1. Changed the rewrite rule for cyclic groups. Previously it was defined
by c…

czf_itt_cyclic_group.mli

3558

19 years 
xiny 
1. Changed the rewrite rule for cyclic groups. Previously it was defined
by c…

czf_itt_cyclic_group.prla

3558

19 years 
xiny 
1. Changed the rewrite rule for cyclic groups. Previously it was defined
by c…

czf_itt_cyclic_subgroup.ml

3570

19 years 
xiny 
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. Th…

czf_itt_cyclic_subgroup.mli

3570

19 years 
xiny 
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. Th…

czf_itt_cyclic_subgroup.prla

3570

19 years 
xiny 
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. Th…

czf_itt_dall.ml

3306

20 years 
nogin 
src mode dform fixes.

czf_itt_dall.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_dall.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_dexists.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_dexists.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_dexists.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_empty.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_empty.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_empty.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_eq.ml

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_eq.mli

3223

20 years 
nogin 
Finally, I am able to commit what I was getting to
in all these commits over the…

czf_itt_eq.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_equiv.ml

3552

19 years 
xiny 
Removed the introduction rule for "equiv" since it made proofs awkard
and could …

czf_itt_equiv.mli

3549

19 years 
xiny 
1. The original equivTransT was wrong. Changed the original equivTrans1T
and …

czf_itt_equiv.prla

3552

19 years 
xiny 
Removed the introduction rule for "equiv" since it made proofs awkard
and could …

czf_itt_exists.ml

3281

20 years 
nogin 
The redundant "_resource" suffix should not be used in resource names.

czf_itt_exists.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_exists.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_false.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_false.mli

3052

20 years 
jyh 
Two changes.
1. expand () now does sloppy expansion, so that proofs
can…

czf_itt_false.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_fol.mlz

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_fol.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_group.ml

3554

19 years 
xiny 
Removed useless stuffs previously in comments.

czf_itt_group.mli

3553

19 years 
xiny 
1. Added "eqG" to the definition of groups which denotes the equivalence
rela…

czf_itt_group.prla

3553

19 years 
xiny 
1. Added "eqG" to the definition of groups which denotes the equivalence
rela…

czf_itt_group_bvd.ml

3569

19 years 
xiny 
Defined "group builder" group_bvd{'h; 'g; 's} which build a group
h from group g…

czf_itt_group_bvd.mli

3569

19 years 
xiny 
Defined "group builder" group_bvd{'h; 'g; 's} which build a group
h from group g…

czf_itt_group_bvd.prla

3569

19 years 
xiny 
Defined "group builder" group_bvd{'h; 'g; 's} which build a group
h from group g…

czf_itt_hom.ml

3559

19 years 
xiny 
Changed def of homomorphisms and reproved all rules;
Added tactics "homIdT" and …

czf_itt_hom.mli

3559

19 years 
xiny 
Changed def of homomorphisms and reproved all rules;
Added tactics "homIdT" and …

czf_itt_hom.prla

3559

19 years 
xiny 
Changed def of homomorphisms and reproved all rules;
Added tactics "homIdT" and …

czf_itt_implies.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_implies.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_implies.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_infinity.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_inv_image.ml

3567

19 years 
xiny 
1. Redefined inverse image. Previously it was defined by introduction
and eli…

czf_itt_inv_image.mli

3567

19 years 
xiny 
1. Redefined inverse image. Previously it was defined by introduction
and eli…

czf_itt_inv_image.prla

3567

19 years 
xiny 
1. Redefined inverse image. Previously it was defined by introduction
and eli…

czf_itt_isect.ml

3281

20 years 
nogin 
The redundant "_resource" suffix should not be used in resource names.

czf_itt_isect.mli

3223

20 years 
nogin 
Finally, I am able to commit what I was getting to
in all these commits over the…

czf_itt_isect.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_member.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_member.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_member.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_nat.ml

3329

20 years 
nogin 
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theor…

czf_itt_nat.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_nat.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_or.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_or.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_or.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_pair.ml

3281

20 years 
nogin 
The redundant "_resource" suffix should not be used in resource names.

czf_itt_pair.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_pair.prla

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_power.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_power.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_power.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_pre_theory.prla

3052

20 years 
jyh 
Two changes.
1. expand () now does sloppy expansion, so that proofs
can…

czf_itt_rel.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_rel.mli

3057

20 years 
jyh 
This jumbo update is a documentation update. There are no
logical changes. I d…

czf_itt_rel.prla

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_sall.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_sall.mli

3052

20 years 
jyh 
Two changes.
1. expand () now does sloppy expansion, so that proofs
can…

czf_itt_sall.prla

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_sep.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_sep.mli

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_sep.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_set.ml

3323

20 years 
kopylov 
Fix some proofs

czf_itt_set.mli

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_set.prla

3323

20 years 
kopylov 
Fix some proofs

czf_itt_set_bvd.ml

3568

19 years 
xiny 
Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are
both metho…

czf_itt_set_bvd.mli

3568

19 years 
xiny 
Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are
both metho…

czf_itt_set_bvd.prla

3568

19 years 
xiny 
Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are
both metho…

czf_itt_set_ind.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_set_ind.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_itt_set_ind.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_itt_setdiff.ml

3380

19 years 
xiny 
Definitions for set difference & Boolean set

czf_itt_setdiff.mli

3380

19 years 
xiny 
Definitions for set difference & Boolean set

czf_itt_setdiff.prla

3380

19 years 
xiny 
Definitions for set difference & Boolean set

czf_itt_sexists.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_sexists.mli

3052

20 years 
jyh 
Two changes.
1. expand () now does sloppy expansion, so that proofs
can…

czf_itt_sexists.prla

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_singleton.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_singleton.mli

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_singleton.prla

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_subgroup.ml

3570

19 years 
xiny 
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. Th…

czf_itt_subgroup.mli

3570

19 years 
xiny 
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. Th…

czf_itt_subgroup.prla

3570

19 years 
xiny 
Updated the definition of subgroups and cyclic subgroups utilizing
group_bvd. Th…

czf_itt_subset.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_subset.mli

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_subset.prla

3239

20 years 
nogin 
CZF: renamed squashrelated tactics, but haven't checked that all proofs
will ex…

czf_itt_theory.mlz

3223

20 years 
nogin 
Finally, I am able to commit what I was getting to
in all these commits over the…

czf_itt_theory.prla

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_true.ml

3292

20 years 
nogin 
*** IMPORTANT: before doing "cvs update" see warning below ***
This commit impl…

czf_itt_true.mli

3052

20 years 
jyh 
Two changes.
1. expand () now does sloppy expansion, so that proofs
can…

czf_itt_true.prla

3058

20 years 
jyh 
Last commit failed partway through...

czf_itt_union.ml

3281

20 years 
nogin 
The redundant "_resource" suffix should not be used in resource names.

czf_itt_union.mli

3223

20 years 
nogin 
Finally, I am able to commit what I was getting to
in all these commits over the…

czf_itt_union.prla

3315

20 years 
nogin 
I have changed the way autoT works.
Now autoT and trivialT share the same auto_…

czf_member.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_or.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_struct.mli

2652

22 years 
kopylov 
1) Added a bug list into BUGS
2) Changed the keywords:
axiom > rule (.mli fil…

czf_theory.mli

2494

22 years 
jyh 
I changed all the obvious places of NuprlLight, NL, nl, or any
other instance t…
