Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-12 11:36:50 -0700 (Fri, 12 Jun 1998)
Revision: 2226
Log message:

      Working factorial proof.
      

Changes	Path
+26 -1	metaprl/editor/ml/test.ml
+7 -0	metaprl/editor/ml/test.mli
+7 -3	metaprl/editor/ml/x.ml
+11 -3	metaprl/filter/filter_cache_fun.ml
+3 -0	metaprl/filter/filter_summary_util.ml
+3 -1	metaprl/mllib/debug.ml
+5 -1	metaprl/mllib/list_util.ml
+9 -0	metaprl/refiner/refbase/opname.ml
+7 -0	metaprl/refiner/refbase/opname.mli
+10 -12	metaprl/refiner/reflib/dform.ml
+2 -1	metaprl/theories/itt/Makefile
+34 -2	metaprl/theories/itt/itt_bool.ml
+11 -2	metaprl/theories/itt/itt_bool.mli
+5 -3	metaprl/theories/itt/itt_int.ml
+6 -2	metaprl/theories/itt/itt_int.mli
Added	metaprl/theories/itt/itt_int_bool.ml
Properties	metaprl/theories/itt/itt_int_bool.ml
Added	metaprl/theories/itt/itt_int_bool.mli
Properties	metaprl/theories/itt/itt_int_bool.mli
+5 -0	metaprl/theories/itt/itt_rfun.ml
+4 -0	metaprl/theories/itt/itt_theory.mlz
+61 -7	metaprl/theories/tactic/conversionals.ml
+20 -0	metaprl/theories/tactic/conversionals.mli
+10 -1	metaprl/theories/tactic/tactic_type.ml