# HG changeset patch
# User wenzelm
# Date 1210280835 -7200
# Node ID e6fe036ec21d5a5b400c2f3f2bf014cc61a9614c
# Parent  7c749112261cc3c709fd0de94fbe0f2fd7e1b10c
updated generated file;

diff -r 7c749112261c -r e6fe036ec21d doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 23:02:23 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Thu May 08 23:07:15 2008 +0200
@@ -871,9 +871,8 @@
   as would be by the proper \mbox{\isa{induct}} and \mbox{\isa{cases}} proof
   methods (see \secref{sec:cases-induct}).
   
-  \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}] provide an interface to the internal
-  \texttt{mk_cases} operation.  Rules are simplified in an
-  unrestricted forward manner.
+  \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
+  forward manner.
 
   While \mbox{\isa{ind{\isacharunderscore}cases}} is a proof method to apply the
   result immediately as elimination rules, \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} provides case split theorems at the theory level
diff -r 7c749112261c -r e6fe036ec21d doc-src/IsarRef/Thy/document/intro.tex
--- a/doc-src/IsarRef/Thy/document/intro.tex	Thu May 08 23:02:23 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex	Thu May 08 23:07:15 2008 +0200
@@ -164,7 +164,7 @@
   directory of Proof~General.
 
   \medskip Apart from the Isabelle command line, defaults for
-  interface options may be given by the \texttt{PROOFGENERAL_OPTIONS}
+  interface options may be given by the \verb|PROOFGENERAL_OPTIONS|
   setting.  For example, the Emacs executable to be used may be
   configured in Isabelle's settings like this:
 \begin{ttbox}
@@ -174,9 +174,10 @@
   Occasionally, a user's \verb|~/.emacs| file contains code
   that is incompatible with the (X)Emacs version used by
   Proof~General, causing the interface startup to fail prematurely.
-  Here the \texttt{-u false} option helps to get the interface process
-  up and running.  Note that additional Lisp customization code may
-  reside in \texttt{proofgeneral-settings.el} of \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
+  Here the \verb|-u false| option helps to get the interface
+  process up and running.  Note that additional Lisp customization
+  code may reside in \verb|proofgeneral-settings.el| of
+  \verb|$ISABELLE_HOME/etc| or \verb|$ISABELLE_HOME_USER/etc|.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -187,10 +188,10 @@
 \begin{isamarkuptext}%
 Proof~General incorporates a version of the Emacs X-Symbol package
   \cite{x-symbol}, which handles proper mathematical symbols displayed
-  on screen.  Pass option \texttt{-x true} to the Isabelle interface
-  script, or check the appropriate Proof~General menu setting by hand.
-  The main challenge of getting X-Symbol to work properly is the
-  underlying (semi-automated) X11 font setup.
+  on screen.  Pass option \verb|-x true| to the Isabelle
+  interface script, or check the appropriate Proof~General menu
+  setting by hand.  The main challenge of getting X-Symbol to work
+  properly is the underlying (semi-automated) X11 font setup.
 
   \medskip Using proper mathematical symbols in Isabelle theories can
   be very convenient for readability of large formulas.  On the other
@@ -264,7 +265,7 @@
   isatool mkdir Foo
 \end{ttbox}
   to initialize a separate directory for session \verb|Foo| ---
-  it is safe to experiment, since \texttt{isatool mkdir} never
+  it is safe to experiment, since \verb|isatool mkdir| never
   overwrites existing files.  Ensure that \verb|Foo/ROOT.ML|
   holds ML commands to load all theories required for this session;
   furthermore \verb|Foo/document/root.tex| should include any