Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-12-29 12:14:09 -0800 (Tue, 29 Dec 1998)
Revision: 2528
Log message:

      Added "kreitz" command to fold up an entire proof subtree into a single node.
      

Changes  Path
+69 -0 metaprl/editor/ml/proof.ml
+6 -0 metaprl/editor/ml/proof.mli
+1 -0 metaprl/editor/ml/proof_edit.ml
+1 -0 metaprl/editor/ml/proof_edit.mli
+9 -1 metaprl/editor/ml/shell.ml
+1 -0 metaprl/editor/ml/shell.mli
+2 -1 metaprl/editor/ml/shell_null.ml
+5 -1 metaprl/editor/ml/shell_rewrite.ml
+5 -1 metaprl/editor/ml/shell_rule.ml
+2 -1 metaprl/editor/ml/shell_type.mlz
+6 -5 metaprl/refiner/reflib/dform.ml
Binary metaprl/theories/reflect_itt/refl_term.prlb