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

      Proof expansion works.
      Fixed a bad typo in red_black_set.
      

Changes	Path
+28 -5	metaprl/editor/ml/io_proof.ml
+8 -4	metaprl/editor/ml/io_proof.mli
+16 -13	metaprl/editor/ml/package_df.ml
+24 -6	metaprl/editor/ml/package_info.ml
+6 -5	metaprl/editor/ml/package_type.mlz
+41 -34	metaprl/editor/ml/proof.ml
+12 -5	metaprl/editor/ml/proof.mli
+6 -0	metaprl/editor/ml/proof_edit.ml
+1 -0	metaprl/editor/ml/proof_edit.mli
+8 -6	metaprl/editor/ml/proof_step.ml
+5 -4	metaprl/editor/ml/proof_step.mli
+16 -4	metaprl/editor/ml/shell.ml
+4 -0	metaprl/editor/ml/shell_mp.ml
+2 -2	metaprl/editor/ml/w.ml
+3 -2	metaprl/editor/ml/y.ml
+18 -10	metaprl/mllib/red_black_set.ml
+2 -1	metaprl/theories/tactic/rewrite_type.ml