Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-17 08:39:32 -0700 (Fri, 17 Jul 1998)
Revision: 2333
Log message:

      CZF is complete, although we may wish to add pairing and inf.
      

Changes	Path
+1 -8	metaprl/editor/ml/nl
+11 -94	metaprl/editor/ml/package_info.ml
+1 -1	metaprl/editor/ml/package_info.mli
+2 -4	metaprl/editor/ml/proof.ml
+1 -1	metaprl/editor/ml/proof.mli
+57 -10	metaprl/editor/ml/proof_step.ml
+0 -1	metaprl/editor/ml/proof_step.mli
+10 -8	metaprl/editor/ml/y.ml
+2 -1	metaprl/filter/filter_bin.ml
+5 -5	metaprl/filter/filter_cache_fun.ml
+3 -2	metaprl/filter/filter_parse.ml
+6 -6	metaprl/filter/filter_summary_type.mlz
+1 -1	metaprl/mk/config
+0 -1	metaprl/mllib/Makefile
+39 -11	metaprl/mllib/file_base.ml
+13 -5	metaprl/mllib/file_base_type.ml
+1 -1	metaprl/refiner/reflib/dform.ml
+10 -1	metaprl/theories/czf/Makefile
+38 -79	metaprl/theories/czf/czf_itt_all.ml
+21 -35	metaprl/theories/czf/czf_itt_all.mli
Binary	metaprl/theories/czf/czf_itt_all.prlb
+37 -25	metaprl/theories/czf/czf_itt_axioms.ml
+5 -37	metaprl/theories/czf/czf_itt_axioms.mli
Binary	metaprl/theories/czf/czf_itt_axioms.prlb
Properties	metaprl/theories/czf/czf_itt_axioms.prlb
+77 -48	metaprl/theories/czf/czf_itt_dall.ml
+24 -29	metaprl/theories/czf/czf_itt_dall.mli
Binary	metaprl/theories/czf/czf_itt_dall.prlb
+65 -51	metaprl/theories/czf/czf_itt_dexists.ml
+31 -32	metaprl/theories/czf/czf_itt_dexists.mli
Binary	metaprl/theories/czf/czf_itt_dexists.prlb
+27 -3	metaprl/theories/czf/czf_itt_eq.ml
+6 -2	metaprl/theories/czf/czf_itt_eq.mli
Added	metaprl/theories/czf/czf_itt_eq_inner.ml
Properties	metaprl/theories/czf/czf_itt_eq_inner.ml
Added	metaprl/theories/czf/czf_itt_eq_inner.mli
Properties	metaprl/theories/czf/czf_itt_eq_inner.mli
Binary	metaprl/theories/czf/czf_itt_eq_inner.prlb
Properties	metaprl/theories/czf/czf_itt_eq_inner.prlb
+88 -85	metaprl/theories/czf/czf_itt_exists.ml
+36 -45	metaprl/theories/czf/czf_itt_exists.mli
Binary	metaprl/theories/czf/czf_itt_exists.prlb
Properties	metaprl/theories/czf/czf_itt_exists.prlb
Added	metaprl/theories/czf/czf_itt_pre_set.ml
Properties	metaprl/theories/czf/czf_itt_pre_set.ml
Added	metaprl/theories/czf/czf_itt_pre_set.mli
Properties	metaprl/theories/czf/czf_itt_pre_set.mli
Binary	metaprl/theories/czf/czf_itt_pre_set.prlb
Properties	metaprl/theories/czf/czf_itt_pre_set.prlb
Added	metaprl/theories/czf/czf_itt_rel.ml
Properties	metaprl/theories/czf/czf_itt_rel.ml
Added	metaprl/theories/czf/czf_itt_rel.mli
Properties	metaprl/theories/czf/czf_itt_rel.mli
Binary	metaprl/theories/czf/czf_itt_rel.prlb
Properties	metaprl/theories/czf/czf_itt_rel.prlb
+36 -56	metaprl/theories/czf/czf_itt_sall.ml
+29 -29	metaprl/theories/czf/czf_itt_sall.mli
Binary	metaprl/theories/czf/czf_itt_sall.prlb
Properties	metaprl/theories/czf/czf_itt_sall.prlb
+9 -0	metaprl/theories/czf/czf_itt_sep.ml
+9 -0	metaprl/theories/czf/czf_itt_sep.mli
+22 -2	metaprl/theories/czf/czf_itt_set.ml
+10 -2	metaprl/theories/czf/czf_itt_set.mli
Binary	metaprl/theories/czf/czf_itt_set.prlb
Added	metaprl/theories/czf/czf_itt_set_ext.ml
Properties	metaprl/theories/czf/czf_itt_set_ext.ml
Added	metaprl/theories/czf/czf_itt_set_ext.mli
Properties	metaprl/theories/czf/czf_itt_set_ext.mli
+125 -28	metaprl/theories/czf/czf_itt_set_ind.ml
+32 -27	metaprl/theories/czf/czf_itt_set_ind.mli
Binary	metaprl/theories/czf/czf_itt_set_ind.prlb
Properties	metaprl/theories/czf/czf_itt_set_ind.prlb
+36 -56	metaprl/theories/czf/czf_itt_sexists.ml
+17 -42	metaprl/theories/czf/czf_itt_sexists.mli
Binary	metaprl/theories/czf/czf_itt_sexists.prlb
Properties	metaprl/theories/czf/czf_itt_sexists.prlb
+1 -8	metaprl/theories/czf/czf_itt_union.ml
+1 -9	metaprl/theories/czf/czf_itt_union.mli
Binary	metaprl/theories/czf/czf_itt_union.prlb
+7 -0	metaprl/theories/itt/itt_equal.ml
+4 -0	metaprl/theories/itt/itt_equal.mli
+64 -2	metaprl/theories/itt/itt_logic.ml
+12 -0	metaprl/theories/itt/itt_logic.mli
+43 -4	metaprl/theories/itt/itt_quotient.ml
+10 -0	metaprl/theories/itt/itt_quotient.mli