1.1 --- a/doc-src/ZF/FOL.tex	Wed Aug 20 11:12:48 2003 +0200
     1.2 +++ b/doc-src/ZF/FOL.tex	Wed Aug 20 13:05:22 2003 +0200
     1.3 @@ -259,8 +259,9 @@
     1.4  IntPr.fast_tac      : int -> tactic
     1.5  IntPr.best_tac      : int -> tactic
     1.6  \end{ttbox}
     1.7 -Most of these belong to the structure \ML{} \texttt{IntPr} and resemble the
     1.8 -tactics of Isabelle's classical reasoner.  Note that you can use the 
     1.9 +Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the
    1.10 +tactics of Isabelle's classical reasoner.  There are no corresponding
    1.11 +Isar methods, but you can use the 
    1.12  \isa{tactic} method to call \ML{} tactics in an Isar script:
    1.13  \begin{isabelle}
    1.14  \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})
    1.15 @@ -350,12 +351,14 @@
    1.16  
    1.17  
    1.18  \section{An intuitionistic example}
    1.19 -Here is a session similar to one in {\em Logic and Computation}
    1.20 -\cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently
    1.21 -from {\sc lcf}-based theorem provers such as {\sc hol}.  
    1.22 +Here is a session similar to one in the book {\em Logic and Computation}
    1.23 +\cite[pages~222--3]{paulson87}. It illustrates the treatment of
    1.24 +quantifier reasoning, which is different in Isabelle than it is in
    1.25 +{\sc lcf}-based theorem provers such as {\sc hol}.  
    1.26  
    1.27 -The theory header must specify that we are working in intuitionistic
    1.28 -logic:
    1.29 +The theory header specifies that we are working in intuitionistic
    1.30 +logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
    1.31 +theory:
    1.32  \begin{isabelle}
    1.33  \isacommand{theory}\ IFOL\_examples\ =\ IFOL:
    1.34  \end{isabelle}
    1.35 @@ -524,7 +527,7 @@
    1.36  $\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
    1.37  follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
    1.38  $\all{x}P(x)$ is true.  Either way the theorem holds.  First, we must
    1.39 -work in a theory based on classical logic:
    1.40 +work in a theory based on classical logic, the theory \isa{FOL}:
    1.41  \begin{isabelle}
    1.42  \isacommand{theory}\ FOL\_examples\ =\ FOL:
    1.43  \end{isabelle}