--- a/doc-src/Intro/getting.tex Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Intro/getting.tex Mon Aug 28 13:52:38 2000 +0200
@@ -26,7 +26,7 @@
isabelle FOL
\end{ttbox}
Note that just typing \texttt{isabelle} usually brings up higher-order logic
-(\HOL) by default.
+(HOL) by default.
\subsection{Lexical matters}
@@ -110,8 +110,8 @@
t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
\end{array}
\]
-Note that \HOL{} uses its traditional ``higher-order'' syntax for application,
-which differs from that used in \FOL\@.
+Note that HOL uses its traditional ``higher-order'' syntax for application,
+which differs from that used in FOL.
The theorems and rules of an object-logic are represented by theorems in
the meta-logic, which are expressed using meta-formulae. Since the
@@ -228,10 +228,10 @@
to have subscript zero, improving readability and reducing subscript
growth.
\end{ttdescription}
-The rules of a theory are normally bound to \ML\ identifiers. Suppose we
-are running an Isabelle session containing theory~\FOL, natural deduction
-first-order logic.\footnote{For a listing of the \FOL{} rules and their
- \ML{} names, turn to
+The rules of a theory are normally bound to \ML\ identifiers. Suppose we are
+running an Isabelle session containing theory~FOL, natural deduction
+first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
+ names, turn to
\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
{page~\pageref{fol-rules}}.}
Let us try an example given in~\S\ref{joining}. We