Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-13 14:11:25 -0700 (Mon, 13 Apr 1998)
Revision: 2122
Log message:

      Added interactive proofs to filter.
      

Changes  Path
+1 -1 metaprl/editor/ml/Makefile
+74 -125 metaprl/editor/ml/proof.ml
+6 -17 metaprl/editor/ml/proof.mli
+20 -117 metaprl/editor/ml/proof_step.ml
+7 -24 metaprl/editor/ml/proof_step.mli
+15 -15 metaprl/filter/Makefile
+19 -5 metaprl/filter/proof_type.mlz
+6 -0 metaprl/mk/config
+1 -1 metaprl/mllib/Makefile
+1 -1 metaprl/refiner/Makefile
+1 -1 metaprl/theories/base/Makefile
+1 -1 metaprl/theories/itt/Makefile
+1 -1 metaprl/theories/tactic/Makefile
+6 -13 metaprl/theories/tactic/tactic_type.mlz
+4 -0 metaprl/theories/tactic/tacticals.ml
Added metaprl/util/Makefile
Properties metaprl/util/Makefile
Added metaprl/util/misc.ml
Properties metaprl/util/misc.ml
Added metaprl/util/misc.mli
Properties metaprl/util/misc.mli
Added metaprl/util/ocamldep.mll
Properties metaprl/util/ocamldep.mll