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