doc-src/Ref/introduction.tex
changeset 9695 ec7d7f877712
parent 9231 8812a07d52ee
child 12831 a2a3896f9c48
--- a/doc-src/Ref/introduction.tex	Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Ref/introduction.tex	Mon Aug 28 13:52:38 2000 +0200
@@ -34,7 +34,7 @@
 \({\langle}isabellehome{\rangle}\)/bin/isabelle
 \end{ttbox}
 This should start an interactive \ML{} session with the default object-logic
-(usually {\HOL}) already pre-loaded.
+(usually HOL) already pre-loaded.
 
 Subsequently, we assume that the \texttt{isabelle} executable is determined
 automatically by the shell, e.g.\ by adding {\tt \(\langle isabellehome
@@ -52,7 +52,7 @@
 isabelle FOL
 \end{ttbox}
 This should put you into the world of polymorphic first-order logic (assuming
-that an image of {\FOL} has been pre-built).
+that an image of FOL has been pre-built).
 
 \index{saving your session|bold} Isabelle provides no means of storing
 theorems or internal proof objects on files.  Theorems are simply part of the
@@ -62,7 +62,7 @@
 \emph{writable} in the first place.  The standard object-logic images are
 usually read-only, so you have to create a private working copy first.  For
 example, the following shell command puts you into a writable Isabelle session
-of name \texttt{Foo} that initially contains just plain \HOL:
+of name \texttt{Foo} that initially contains just plain HOL:
 \begin{ttbox}
 isabelle HOL Foo
 \end{ttbox}
@@ -202,7 +202,7 @@
   
 \end{ttdescription}
 
-Note that theories of pre-built logic images (e.g.\ {\HOL}) are marked as
+Note that theories of pre-built logic images (e.g.\ HOL) are marked as
 \emph{finished} and cannot be updated any more.  See \S\ref{sec:more-theories}
 for further information on Isabelle's theory loader.