Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-17 18:43:40 -0700 (Thu, 17 Apr 2003)
Revision: 4447
Log message:

      - Instead of always using {\bf ...}, {\it ...}, etc, now @tt uses \texttt{...}
      in text mode and \mathtt{...} in math mode.
      - The comment parser now knows that @mbox and @hbox take you out of math mode.
      

Changes  Path
+2 -3 metaprl/README
+17 -13 metaprl/mllib/comment_parse.mll
+3 -3 metaprl/theories/base/base_dtactic.ml
+2 -2 metaprl/theories/itt/itt_dprod.ml
+1 -1 metaprl/theories/itt/itt_record.ml
+16 -16 metaprl/theories/tactic/comment.ml
+1 -1 metaprl/theories/tactic/comment.mli
+4 -4 metaprl/theories/tactic/nuprl_font.ml
+1 -1 texinputs/metaprl.tex