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

Index of /metaprl/theories/czf

Files shown:132
Directory revision: 3553 (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  3548  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  3544  19 years  xiny   Changed the definition of abelian groups completely. An abelian group is now def…
czf_itt_abel_group.mli  3544  19 years  xiny   Changed the definition of abelian groups completely. An abelian group is now def…
czf_itt_abel_group.prla  3544  19 years  xiny   Changed the definition of abelian groups completely. An abelian group is now def…
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  3538  19 years  xiny   1. Changed the definition of cyclic groups from cyclic_group{'g;'a} which rep…
czf_itt_cyclic_group.mli  3538  19 years  xiny   1. Changed the definition of cyclic groups from cyclic_group{'g;'a} which rep…
czf_itt_cyclic_group.prla  3538  19 years  xiny   1. Changed the definition of cyclic groups from cyclic_group{'g;'a} which rep…
czf_itt_cyclic_subgroup.ml  3537  19 years  xiny   1. Changed the definition of cyclic subgroups from cyclic_subgroup{'g; 'a} to…
czf_itt_cyclic_subgroup.mli  3537  19 years  xiny   1. Changed the definition of cyclic subgroups from cyclic_subgroup{'g; 'a} to…
czf_itt_cyclic_subgroup.prla  3539  19 years  xiny   This completes the committion of czf_itt_cyclic_subgroup.
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  3553  19 years  xiny   1. Added "eqG" to the definition of groups which denotes the equivalence rela…
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_hom.ml  3547  19 years  xiny   Defined homomorphism for groups. A map f of a group G into a group G' is a homom…
czf_itt_hom.mli  3547  19 years  xiny   Defined homomorphism for groups. A map f of a group G into a group G' is a homom…
czf_itt_hom.prla  3547  19 years  xiny   Defined homomorphism for groups. A map f of a group G into a group G' is a homom…
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  3546  19 years  xiny   Added the module for the inverse image of set t in set s under function f: { …
czf_itt_inv_image.mli  3546  19 years  xiny   Added the module for the inverse image of set t in set s under function f: { …
czf_itt_inv_image.prla  3546  19 years  xiny   Added the module for the inverse image of set t in set s under function f: { …
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  3545  19 years  xiny   Added the definition for "set builder", i.e., the image of a set s under some fu…
czf_itt_set_bvd.mli  3545  19 years  xiny   Added the definition for "set builder", i.e., the image of a set s under some fu…
czf_itt_set_bvd.prla  3545  19 years  xiny   Added the definition for "set builder", i.e., the image of a set s under some fu…
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  3536  19 years  xiny   1. Changed the definition of subgroup{'g; 's}; 's is now a "label" instead of…
czf_itt_subgroup.mli  3536  19 years  xiny   1. Changed the definition of subgroup{'g; 's}; 's is now a "label" instead of…
czf_itt_subgroup.prla  3536  19 years  xiny   1. Changed the definition of subgroup{'g; 's}; 's is now a "label" instead of…
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