1.1 --- a/doc-src/Intro/getting.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/Intro/getting.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  isabelle FOL
     1.5  \end{ttbox}
     1.6  Note that just typing \texttt{isabelle} usually brings up higher-order logic
     1.7 -(\HOL) by default.
     1.8 +(HOL) by default.
     1.9  
    1.10  
    1.11  \subsection{Lexical matters}
    1.12 @@ -110,8 +110,8 @@
    1.13    t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)}
    1.14  \end{array}  
    1.15  \]
    1.16 -Note that \HOL{} uses its traditional ``higher-order'' syntax for application,
    1.17 -which differs from that used in \FOL\@.
    1.18 +Note that HOL uses its traditional ``higher-order'' syntax for application,
    1.19 +which differs from that used in FOL.
    1.20  
    1.21  The theorems and rules of an object-logic are represented by theorems in
    1.22  the meta-logic, which are expressed using meta-formulae.  Since the
    1.23 @@ -228,10 +228,10 @@
    1.24    to have subscript zero, improving readability and reducing subscript
    1.25    growth.
    1.26  \end{ttdescription}
    1.27 -The rules of a theory are normally bound to \ML\ identifiers.  Suppose we
    1.28 -are running an Isabelle session containing theory~\FOL, natural deduction
    1.29 -first-order logic.\footnote{For a listing of the \FOL{} rules and their
    1.30 -  \ML{} names, turn to
    1.31 +The rules of a theory are normally bound to \ML\ identifiers.  Suppose we are
    1.32 +running an Isabelle session containing theory~FOL, natural deduction
    1.33 +first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
    1.34 +  names, turn to
    1.35  \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}%
    1.36             {page~\pageref{fol-rules}}.}
    1.37  Let us try an example given in~\S\ref{joining}.  We