replaced some latex macros by antiquotations;
authorwenzelm
Thu May 08 23:02:23 2008 +0200 (2008-05-08)
changeset 268607c749112261c
parent 26859 b9ab6246765e
child 26861 e6fe036ec21d
replaced some latex macros by antiquotations;
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/intro.thy
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 22:49:05 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Thu May 08 23:02:23 2008 +0200
     1.3 @@ -868,9 +868,9 @@
     1.4    methods (see \secref{sec:cases-induct}).
     1.5    
     1.6    \item [@{method (HOL) ind_cases} and @{command (HOL)
     1.7 -  "inductive_cases"}] provide an interface to the internal
     1.8 -  \texttt{mk_cases} operation.  Rules are simplified in an
     1.9 -  unrestricted forward manner.
    1.10 +  "inductive_cases"}] provide an interface to the internal @{ML_text
    1.11 +  mk_cases} operation.  Rules are simplified in an unrestricted
    1.12 +  forward manner.
    1.13  
    1.14    While @{method (HOL) ind_cases} is a proof method to apply the
    1.15    result immediately as elimination rules, @{command (HOL)
     2.1 --- a/doc-src/IsarRef/Thy/intro.thy	Thu May 08 22:49:05 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/intro.thy	Thu May 08 23:02:23 2008 +0200
     2.3 @@ -140,7 +140,7 @@
     2.4    directory of Proof~General.
     2.5  
     2.6    \medskip Apart from the Isabelle command line, defaults for
     2.7 -  interface options may be given by the \texttt{PROOFGENERAL_OPTIONS}
     2.8 +  interface options may be given by the @{verbatim PROOFGENERAL_OPTIONS}
     2.9    setting.  For example, the Emacs executable to be used may be
    2.10    configured in Isabelle's settings like this:
    2.11  \begin{ttbox}
    2.12 @@ -150,10 +150,11 @@
    2.13    Occasionally, a user's @{verbatim "~/.emacs"} file contains code
    2.14    that is incompatible with the (X)Emacs version used by
    2.15    Proof~General, causing the interface startup to fail prematurely.
    2.16 -  Here the \texttt{-u false} option helps to get the interface process
    2.17 -  up and running.  Note that additional Lisp customization code may
    2.18 -  reside in \texttt{proofgeneral-settings.el} of @{verbatim
    2.19 -  "$ISABELLE_HOME/etc"} or @{verbatim "$ISABELLE_HOME_USER/etc"}.
    2.20 +  Here the @{verbatim "-u false"} option helps to get the interface
    2.21 +  process up and running.  Note that additional Lisp customization
    2.22 +  code may reside in @{verbatim "proofgeneral-settings.el"} of
    2.23 +  @{verbatim "$ISABELLE_HOME/etc"} or @{verbatim
    2.24 +  "$ISABELLE_HOME_USER/etc"}.
    2.25  *}
    2.26  
    2.27  
    2.28 @@ -162,10 +163,10 @@
    2.29  text {*
    2.30    Proof~General incorporates a version of the Emacs X-Symbol package
    2.31    \cite{x-symbol}, which handles proper mathematical symbols displayed
    2.32 -  on screen.  Pass option \texttt{-x true} to the Isabelle interface
    2.33 -  script, or check the appropriate Proof~General menu setting by hand.
    2.34 -  The main challenge of getting X-Symbol to work properly is the
    2.35 -  underlying (semi-automated) X11 font setup.
    2.36 +  on screen.  Pass option @{verbatim "-x true"} to the Isabelle
    2.37 +  interface script, or check the appropriate Proof~General menu
    2.38 +  setting by hand.  The main challenge of getting X-Symbol to work
    2.39 +  properly is the underlying (semi-automated) X11 font setup.
    2.40  
    2.41    \medskip Using proper mathematical symbols in Isabelle theories can
    2.42    be very convenient for readability of large formulas.  On the other
    2.43 @@ -235,7 +236,7 @@
    2.44    isatool mkdir Foo
    2.45  \end{ttbox}
    2.46    to initialize a separate directory for session @{verbatim Foo} ---
    2.47 -  it is safe to experiment, since \texttt{isatool mkdir} never
    2.48 +  it is safe to experiment, since @{verbatim "isatool mkdir"} never
    2.49    overwrites existing files.  Ensure that @{verbatim "Foo/ROOT.ML"}
    2.50    holds ML commands to load all theories required for this session;
    2.51    furthermore @{verbatim "Foo/document/root.tex"} should include any