/[mojave]/metaprl/theories/czf
ViewVC logotype

Index of /metaprl/theories/czf

Files shown:135
Directory revision: 3570 (of 13286)
Sticky Revision:


File Rev. Age Author Last log entry
 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 squash-related 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 Nuprl-Light, NL, nl, or any other instance t…

Properties

Name Value
svn:ignore .consign *.cm* *.p4* *.pp* *.prlb Makefile.dep gmon.out

  ViewVC Help
Powered by ViewVC 1.1.26