Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-05-20 16:04:08 -0700 (Sun, 20 May 2001)
Revision: 3235
Log message:

      Display form fixes.
      
      - TeX: all object-level terms (theorem statements, etc) are now typeset
      in math mode.
      
      - Tex: variable names are now parsed to detect indeces. In particular,
        'a1 will now be printed as a_{1} and 'a1_2 will be printed as a_{1,2}.
      
      - Tex: `|' symbol in display forms is now always handled correctly.
      
      - Numerous small fixes.
      

Changes  Path
+35 -12 metaprl/refiner/reflib/rformat.ml
+2 -7 metaprl/theories/base/base_rewrite.ml
+20 -30 metaprl/theories/czf/czf_itt_comment.ml
+2 -8 metaprl/theories/czf/czf_itt_sall.ml
+2 -8 metaprl/theories/czf/czf_itt_sexists.ml
+6 -12 metaprl/theories/itt/itt_comment.ml
+0 -1 metaprl/theories/itt/itt_comment.mli
+1 -1 metaprl/theories/itt/itt_dprod.ml
+6 -3 metaprl/theories/itt/itt_equal.ml
+9 -9 metaprl/theories/itt/itt_logic.ml
+1 -1 metaprl/theories/itt/itt_set.ml
+10 -13 metaprl/theories/itt/itt_squash.ml
+12 -12 metaprl/theories/itt/itt_squiggle.ml
+6 -6 metaprl/theories/itt/itt_struct.ml
+2 -2 metaprl/theories/itt/itt_struct2.ml
+1 -1 metaprl/theories/itt/itt_subtype.ml
+73 -25 metaprl/theories/tactic/base_dform.ml
+6 -14 metaprl/theories/tactic/comment.ml
+1 -0 metaprl/theories/tactic/comment.mli
+18 -18 metaprl/theories/tactic/nuprl_font.ml
+0 -2 metaprl/theories/tactic/perv.ml
+22 -17 metaprl/theories/tactic/summary.ml
+4 -4 metaprl/theories/tactic/top_conversionals.ml
+1 -1 metaprl/theories/tactic/top_tacticals.ml
+1 -1 metaprl/theories/tactic/var.ml
+4 -0 texinputs/metaprl.tex