updated generated file;
authorwenzelm
Thu May 08 23:07:15 2008 +0200 (2008-05-08)
changeset 26861e6fe036ec21d
parent 26860 7c749112261c
child 26862 a79d7d5f1d06
updated generated file;
doc-src/IsarRef/Thy/document/HOL_Specific.tex
doc-src/IsarRef/Thy/document/intro.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 23:02:23 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 23:07:15 2008 +0200
     1.3 @@ -871,9 +871,8 @@
     1.4    as would be by the proper \mbox{\isa{induct}} and \mbox{\isa{cases}} proof
     1.5    methods (see \secref{sec:cases-induct}).
     1.6    
     1.7 -  \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}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 +  \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}] provide an interface to the internal \verb|mk_cases| operation.  Rules are simplified in an unrestricted
    1.11 +  forward manner.
    1.12  
    1.13    While \mbox{\isa{ind{\isacharunderscore}cases}} is a proof method to apply the
    1.14    result immediately as elimination rules, \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} provides case split theorems at the theory level
     2.1 --- a/doc-src/IsarRef/Thy/document/intro.tex	Thu May 08 23:02:23 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/intro.tex	Thu May 08 23:07:15 2008 +0200
     2.3 @@ -164,7 +164,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 \verb|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 @@ -174,9 +174,10 @@
    2.13    Occasionally, a user's \verb|~/.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 \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
    2.19 +  Here the \verb|-u false| option helps to get the interface
    2.20 +  process up and running.  Note that additional Lisp customization
    2.21 +  code may reside in \verb|proofgeneral-settings.el| of
    2.22 +  \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
    2.23  \end{isamarkuptext}%
    2.24  \isamarkuptrue%
    2.25  %
    2.26 @@ -187,10 +188,10 @@
    2.27  \begin{isamarkuptext}%
    2.28  Proof~General incorporates a version of the Emacs X-Symbol package
    2.29    \cite{x-symbol}, which handles proper mathematical symbols displayed
    2.30 -  on screen.  Pass option \texttt{-x true} to the Isabelle interface
    2.31 -  script, or check the appropriate Proof~General menu setting by hand.
    2.32 -  The main challenge of getting X-Symbol to work properly is the
    2.33 -  underlying (semi-automated) X11 font setup.
    2.34 +  on screen.  Pass option \verb|-x true| to the Isabelle
    2.35 +  interface script, or check the appropriate Proof~General menu
    2.36 +  setting by hand.  The main challenge of getting X-Symbol to work
    2.37 +  properly is the underlying (semi-automated) X11 font setup.
    2.38  
    2.39    \medskip Using proper mathematical symbols in Isabelle theories can
    2.40    be very convenient for readability of large formulas.  On the other
    2.41 @@ -264,7 +265,7 @@
    2.42    isatool mkdir Foo
    2.43  \end{ttbox}
    2.44    to initialize a separate directory for session \verb|Foo| ---
    2.45 -  it is safe to experiment, since \texttt{isatool mkdir} never
    2.46 +  it is safe to experiment, since \verb|isatool mkdir| never
    2.47    overwrites existing files.  Ensure that \verb|Foo/ROOT.ML|
    2.48    holds ML commands to load all theories required for this session;
    2.49    furthermore \verb|Foo/document/root.tex| should include any