doc-src/System/present.tex
changeset 9695 ec7d7f877712
parent 9237 161fb7f00414
child 10564 42f41f966db4
     1.1 --- a/doc-src/System/present.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/System/present.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  In order to let Isabelle generate theory browsing information, simply append
     1.6  ``\texttt{-i true}'' to the \settdx{ISABELLE_USEDIR_OPTIONS} setting before
     1.7 -making a logic.  For example, in order to do this for {\FOL}, add this to your
     1.8 +making a logic.  For example, in order to do this for FOL, add this to your
     1.9  Isabelle settings file
    1.10  \begin{ttbox}
    1.11  ISABELLE_USEDIR_OPTIONS="-i true"
    1.12 @@ -87,8 +87,8 @@
    1.13  isatool usedir -i true HOL Foo
    1.14  \end{ttbox}
    1.15  This assumes that directory \texttt{Foo} contains some \texttt{ROOT.ML} file
    1.16 -to load all your theories, and {\HOL} is your parent logic image.  Ideally,
    1.17 -theory browser information would have been generated for {\HOL} already.
    1.18 +to load all your theories, and HOL is your parent logic image.  Ideally,
    1.19 +theory browser information would have been generated for HOL already.
    1.20  
    1.21  Alternatively, one may specify an external link to an existing body of HTML
    1.22  data by giving \texttt{usedir} a \texttt{-P} option like this:
    1.23 @@ -499,7 +499,7 @@
    1.24  \medskip Any \texttt{usedir} session is named by some \emph{session
    1.25    identifier}. These accumulate, documenting the way sessions depend on
    1.26  others. For example, consider \texttt{Pure/FOL/ex}, which refers to the
    1.27 -examples of {\FOL}, which in turn is built upon {\Pure}.
    1.28 +examples of FOL, which in turn is built upon Pure.
    1.29  
    1.30  The current session's identifier is by default just the base name of the
    1.31  \texttt{LOGIC} argument (in build mode), or of the \texttt{NAME} argument (in