Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2000-09-23 17:46:18 -0700 (Sat, 23 Sep 2000)
Revision: 3074
Log message:

      Update Itt_logic/implies_df to a nested dform (so it displays recursive
      implications correctly).  Also, fixed a bug in rformat.ml that was causing
      the formatter to calculate the left margin correctly.
      
      I also forgot to mention two new things earlier.  I added the
      cbreak [s1:s; s2:s] display form, which adds a break if the next text
      element would overlow the right margin.  This is useful in text formatting.
      The s1 and s2 are optional; cbreak <--> cbreak[""; " "].  Also, there
      is now a display form pushm[str:s], which adds the text in every
      indentatio, rather than whitespace.  This is useful for comment formatting,
      where the comment lines are indented with the " * " string.
      

Changes	Path
+30 -35	metaprl/refiner/reflib/rformat.ml
+10 -11	metaprl/theories/itt/itt_int_bool_new.ml
+16 -5	metaprl/theories/itt/itt_logic.ml
+38 -37	metaprl/theories/tactic/base_dform.ml