Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-02 19:57:45 -0700 (Tue, 02 Sep 2003)
Revision: 4911
Log message:

      Xin & Aleksey:
      - Fixed and improved a number of display forms.
      - Made a number of improvements to the documentation text.
      - Fixed the recent breakage in Itt_rfun (removed the ``experimental'' rule
      that Xin have added and removed the unneeded assumption from the original rule).
      

Changes  Path
+3 -4 metaprl/filter/filter/term_grammar.ml
+4 -0 metaprl/lib/words
+1 -0 metaprl/refiner/reflib/dform.mli
+3 -1 metaprl/support/display/base_dform.ml
+9 -4 metaprl/support/display/comment.ml
+2 -2 metaprl/support/display/comment.mli
+13 -9 metaprl/support/display/summary.ml
+18 -18 metaprl/support/tactics/top_conversionals.ml
+29 -13 metaprl/support/tactics/top_tacticals.ml
+1 -1 metaprl/theories/base/base_rewrite.ml
+6 -3 metaprl/theories/base/base_theory.mlz
+4 -4 metaprl/theories/czf/czf_itt_theory.mlz
+1 -1 metaprl/theories/experimental/compile/m_ast.ml
+1 -1 metaprl/theories/experimental/compile/m_doc_x86_codegen.ml
+34 -27 metaprl/theories/experimental/compile/m_ir_ast.ml
+7 -9 metaprl/theories/experimental/compile/m_ra_type.mlz
+3 -0 metaprl/theories/itt/itt_atom.ml
+4 -3 metaprl/theories/itt/itt_equal.ml
+3 -3 metaprl/theories/itt/itt_logic.ml
+1 -10 metaprl/theories/itt/itt_rfun.ml
+17 -17 metaprl/theories/itt/itt_struct.ml
+4 -4 metaprl/theories/itt/itt_theory.ml
+1 -1 metaprl/theories/itt/itt_union.ml