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