doc-src/ZF/FOL.tex
changeset 14158 15bab630ae31
parent 14154 3bc0128e2c74
child 30099 dde11464969c
--- a/doc-src/ZF/FOL.tex	Wed Aug 20 11:12:48 2003 +0200
+++ b/doc-src/ZF/FOL.tex	Wed Aug 20 13:05:22 2003 +0200
@@ -259,8 +259,9 @@
 IntPr.fast_tac      : int -> tactic
 IntPr.best_tac      : int -> tactic
 \end{ttbox}
-Most of these belong to the structure \ML{} \texttt{IntPr} and resemble the
-tactics of Isabelle's classical reasoner.  Note that you can use the 
+Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the
+tactics of Isabelle's classical reasoner.  There are no corresponding
+Isar methods, but you can use the 
 \isa{tactic} method to call \ML{} tactics in an Isar script:
 \begin{isabelle}
 \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*})
@@ -350,12 +351,14 @@
 
 
 \section{An intuitionistic example}
-Here is a session similar to one in {\em Logic and Computation}
-\cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently
-from {\sc lcf}-based theorem provers such as {\sc hol}.  
+Here is a session similar to one in the book {\em Logic and Computation}
+\cite[pages~222--3]{paulson87}. It illustrates the treatment of
+quantifier reasoning, which is different in Isabelle than it is in
+{\sc lcf}-based theorem provers such as {\sc hol}.  
 
-The theory header must specify that we are working in intuitionistic
-logic:
+The theory header specifies that we are working in intuitionistic
+logic by designating \isa{IFOL} rather than \isa{FOL} as the parent
+theory:
 \begin{isabelle}
 \isacommand{theory}\ IFOL\_examples\ =\ IFOL:
 \end{isabelle}
@@ -524,7 +527,7 @@
 $\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
 follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
 $\all{x}P(x)$ is true.  Either way the theorem holds.  First, we must
-work in a theory based on classical logic:
+work in a theory based on classical logic, the theory \isa{FOL}:
 \begin{isabelle}
 \isacommand{theory}\ FOL\_examples\ =\ FOL:
 \end{isabelle}