
diff -r 01b87a921967 -r 2ca08f62df33 doc-src/Logics/FOL.tex
--- a/doc-src/Logics/FOL.tex	Fri Apr 22 18:18:37 1994 +0200
+++ b/doc-src/Logics/FOL.tex	Fri Apr 22 18:43:49 1994 +0200
@@ -35,9 +35,9 @@
 Some intuitionistic derived rules are shown in
 Fig.\ts\ref{fol-int-derived}, again with their \ML\ names.  These include
 rules for the defined symbols $\neg$, $\bimp$ and $\exists!$.  Natural
-deduction typically involves a combination of forwards and backwards
+deduction typically involves a combination of forward and backward
 reasoning, particularly with the destruction rules $(\conj E)$,
-$({\imp}E)$, and~$(\forall E)$.  Isabelle's backwards style handles these
+$({\imp}E)$, and~$(\forall E)$.  Isabelle's backward style handles these
 rules badly, so sequent-style rules are derived to eliminate conjunctions,
 implications, and universal quantifiers.  Used with elim-resolution,
 \tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
@@ -45,7 +45,7 @@
 conj_impE}, etc., support the intuitionistic proof procedure
 (see~\S\ref{fol-int-prover}).
 
-See the files {\tt FOL/ifol.thy}, {\tt FOL/ifol.ML} and
+See the files {\tt FOL/IFOL.thy}, {\tt FOL/IFOL.ML} and
 {\tt FOL/intprover.ML} for complete listings of the rules and
 derived rules.
 
@@ -360,7 +360,7 @@
 generally unsuitable for depth-first search.
 \end{ttdescription}
 \noindent
-See the file {\tt FOL/fol.ML} for derivations of the
+See the file {\tt FOL/FOL.ML} for derivations of the
 classical rules, and 
 \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
         {Chap.\ts\ref{chap:classical}} 
@@ -582,7 +582,7 @@
 {\out  1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
 \end{ttbox}
 By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
-effectively applies~$(\exists I)$ again.
+in effect applies~$(\exists I)$ again.
 \begin{ttbox}
 by (eresolve_tac [allE] 1);
 {\out Level 4}
@@ -622,7 +622,7 @@
 {\out EX y. ALL x. P(y) --> P(x)}
 {\out No subgoals!}
 \end{ttbox}
-The civilized way to prove this theorem is through \ttindex{best_tac},
+The civilised way to prove this theorem is through \ttindex{best_tac},
 supplying the classical version of~$(\exists I)$:
 \begin{ttbox}
 goal FOL.thy "EX y. ALL x. P(y)-->P(x)";
@@ -778,8 +778,8 @@
 {\out  3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
 {\out  4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
 \end{ttbox}
-
-In the first two subgoals, all formulae have been reduced to atoms.  Now
+%
+In the first two subgoals, all assumptions have been reduced to atoms.  Now
 $if$-introduction can be applied.  Observe how the $if$-rules break down
 occurrences of $if$ when they become the outermost connective.
 \begin{ttbox}




