diff -r f8701e067e43 -r c15f46833f7a doc-src/Intro/getting.tex
--- a/doc-src/Intro/getting.tex	Tue Apr 07 13:46:34 1998 +0200
+++ b/doc-src/Intro/getting.tex	Thu Apr 09 12:29:39 1998 +0200
@@ -17,9 +17,17 @@
 tacticals have function types such as {\tt tactic->tactic}.  Isabelle
 users can operate on these data structures by writing \ML{} programs.
 
+
 \section{Forward proof}\label{sec:forward} \index{forward proof|(}
 This section describes the concrete syntax for types, terms and theorems,
-and demonstrates forward proof.
+and demonstrates forward proof.  The examples are set in first-order logic.
+The command to start Isabelle running first-order logic is
+\begin{ttbox}
+isabelle FOL
+\end{ttbox}
+Note that just typing \texttt{isabelle} usually brings up higher-order logic
+(\HOL) by default.
+
 
 \subsection{Lexical matters}
 \index{identifiers}\index{reserved words} 
@@ -76,16 +84,15 @@
 \index{*:: symbol}\index{*=> symbol}
 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
 \index{*[ symbol}\index{*] symbol}
-\begin{array}{lll}
-    \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline
-  \alpha "::" C              & \alpha :: C        & \hbox{class constraint} \\
+\begin{array}{ll}
+    \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline
+  \alpha "::" C              & \hbox{class constraint} \\
   \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" &
-     \alpha :: \{C@1,\dots,C@n\}             & \hbox{sort constraint} \\
-  \sigma " => " \tau        & \sigma\To\tau & \hbox{function type} \\
-  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau &
-     [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\
-  "(" \tau@1"," \ldots "," \tau@n ")" tycon & 
-     (\tau@1, \ldots, \tau@n)tycon      & \hbox{type construction}
+        \hbox{sort constraint} \\
+  \sigma " => " \tau        & \hbox{function type } \sigma\To\tau \\
+  "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau 
+       & \hbox{$n$-argument function type} \\
+  "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction}
 \end{array} 
 \]
 Terms are those of the typed $\lambda$-calculus.
@@ -93,16 +100,19 @@
 \[\dquotes
 \index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions}
 \index{*:: symbol}
-\begin{array}{lll}
-    \multicolumn{3}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
-  t "::" \sigma         & t :: \sigma   & \hbox{type constraint} \\
-  "\%" x "." t          & \lambda x.t   & \hbox{abstraction} \\
-  "\%" x@1\ldots x@n "." t  & \lambda x@1\ldots x@n.t & 
-     \hbox{curried abstraction} \\
-  t "(" u@1"," \ldots "," u@n ")" & 
-  t (u@1, \ldots, u@n) & \hbox{curried application}
+\begin{array}{ll}
+    \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline
+  t "::" \sigma         & \hbox{type constraint} \\
+  "\%" x "." t          & \hbox{abstraction } \lambda x.t \\
+  "\%" x@1\ldots x@n "." t  & \hbox{abstraction over several arguments} \\
+  t "(" u@1"," \ldots "," u@n ")" &
+     \hbox{application to several arguments (FOL and ZF)} \\
+  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\@.
+
 The theorems and rules of an object-logic are represented by theorems in
 the meta-logic, which are expressed using meta-formulae.  Since the
 meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{}