--- a/doc-src/Logics/CTT.tex Fri Apr 22 18:18:37 1994 +0200
+++ b/doc-src/Logics/CTT.tex Fri Apr 22 18:43:49 1994 +0200
@@ -395,8 +395,8 @@
Elimination rules have the suffix~{\tt E}\@. Computation rules, which
describe the reduction of eliminators, have the suffix~{\tt C}\@. The
equality versions of the rules (which permit reductions on subterms) are
-called {\em long} rules; their names have the suffix~{\tt L}\@.
-Introduction and computation rules often are further suffixed with
+called {\bf long} rules; their names have the suffix~{\tt L}\@.
+Introduction and computation rules are often further suffixed with
constructor names.
Figure~\ref{ctt-equality} presents the equality rules. Most of them are
@@ -514,12 +514,12 @@
\end{ttbox}
Blind application of {\CTT} rules seldom leads to a proof. The elimination
rules, especially, create subgoals containing new unknowns. These subgoals
-unify with anything, causing an undirectional search. The standard tactic
+unify with anything, creating a huge search space. The standard tactic
\ttindex{filt_resolve_tac}
(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
{\S\ref{filt_resolve_tac}})
%
-can reject overly flexible goals; so does the {\CTT} tactic {\tt
+fails for goals that are too flexible; so does the {\CTT} tactic {\tt
test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they
achieve a simple kind of subgoal reordering: the less flexible subgoals are
attempted first. Do some single step proofs, or study the examples below,
@@ -623,7 +623,7 @@
\item[\ttindexbold{safestep_tac} $thms$ $i$]
attacks subgoal~$i$ using formation rules and certain other `safe' rules
-(tdx{FE}, tdx{ProdI}, tdx{SumE}, tdx{PlusE}), calling
+(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling
{\tt mp_tac} when appropriate. It also uses~$thms$,
which are typically premises of the rule being derived.
@@ -708,7 +708,6 @@
\[ a \bmod b + (a/b)\times b = a. \]
Figure~\ref{ctt-arith} presents the definitions and some of the key
theorems, including commutative, distributive, and associative laws.
-All proofs are on the file {\tt CTT/arith.ML}.
The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
and~\verb'div' stand for sum, difference, absolute difference, product,
@@ -1065,7 +1064,7 @@
function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
In principle, the Axiom of Choice is simple to derive in Constructive Type
-Theory \cite[page~50]{martinlof84}. The following definitions work:
+Theory. The following definitions work:
\begin{eqnarray*}
f & \equiv & {\tt fst} \circ h \\
g & \equiv & {\tt snd} \circ h
--- 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}
--- a/doc-src/Logics/LK.tex Fri Apr 22 18:18:37 1994 +0200
+++ b/doc-src/Logics/LK.tex Fri Apr 22 18:43:49 1994 +0200
@@ -222,7 +222,7 @@
{\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
specifying the formula to duplicate.
-See the files {\tt LK/lk.thy} and {\tt LK/lk.ML}
+See the files {\tt LK/LK.thy} and {\tt LK/LK.ML}
for complete listings of the rules and derived rules.
@@ -296,7 +296,7 @@
\end{ttbox}
Associative unification is not as efficient as it might be, in part because
the representation of lists defeats some of Isabelle's internal
-optimizations. The following operations implement faster rule application,
+optimisations. The following operations implement faster rule application,
and may have other uses.
\begin{ttdescription}
\item[\ttindexbold{forms_of_seq} {\it t}]