/[mojave]/metaprl/theories/tactic/comment.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/comment.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3583 by nogin, Sun May 20 23:04:08 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 44  Line 44 
44   * @end[verbatim]   * @end[verbatim]
45   *   *
46   * There is also a @emph{math} mode, which is entered for terms between   * There is also a @emph{math} mode, which is entered for terms between
47   * @code{$} or @code{$$} forms.  The contents of math mode is   * @tt["$"] or @tt["$$"] forms.  The contents of math mode is
48   * parsed in a similar manner to normal mode, but the `_' and `^' characters   * parsed in a similar manner to normal mode, but the `_' and `^' characters
49   * are significant in math mode (they are normal text in normal mode).   * are significant in math mode (they are normal text in normal mode).
50   * The `_' term identifies a subscript operation, and the `^' term   * The `_' term identifies a subscript operation, and the `^' term
# Line 70  Line 70 
70   * along with this program; if not, write to the Free Software   * along with this program; if not, write to the Free Software
71   * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.   * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
72   *   *
73   * Author: Jason Hickey   * Author: Jason Hickey @email{jyh@cs.caltech.edu}
  * @email{jyh@cs.caltech.edu}  
74   * @end[license]   * @end[license]
75   *)   *)
76    
77  (*  (*!
78   * @begin[doc]   * @begin[doc]
79   * @parents   * @parents
80   * @end[doc]   * @end[doc]
# Line 816  Line 815 
815   * @thysubsection{Math mode}   * @thysubsection{Math mode}
816   *   *
817   * Terms are formatted in @emph{math mode} if they are   * Terms are formatted in @emph{math mode} if they are
818   * placed between matching @code{$} symbols (for inline   * placed between matching @tt["$"] symbols (for inline
819   * math expressions), or matching @code{$$} symbols (for   * math expressions), or matching @tt["$$"] symbols (for
820   * centered math expressions).  All terms in math mode   * centered math expressions).  All terms in math mode
821   * have an @tt{opname} that begins with the prefix @tt{math_}.   * have an @tt{opname} that begins with the prefix @tt{math_}.
822   *   *
# Line 1450  Line 1449 
1449  declare math_defrule{'name; 'args; 'hyps; 'goal}  declare math_defrule{'name; 'args; 'hyps; 'goal}
1450  declare math_rulebox{'tac; 'args; 'hyps; 'goal}  declare math_rulebox{'tac; 'args; 'hyps; 'goal}
1451  declare math_sequent{'ext; 'hyps; 'goal}  declare math_sequent{'ext; 'hyps; 'goal}
1452    (*! @docoff *)
1453    
1454  (*  (*
1455   * TeX display.   * TeX display.
# Line 1506  Line 1506 
1506     slot{'goal}     slot{'goal}
1507     ezone popm     ezone popm
1508    
1509  (*!  (*
1510   * -*-   * -*-
1511   * Local Variables:   * Local Variables:
1512   * Caml-master: "compile"   * Caml-master: "compile"

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26