final Springer copy

--- a/doc-src/Ref/classical.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/classical.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -28,9 +28,10 @@
 be traced, and their components can be called directly; in this manner,
 any proof can be viewed interactively.
 
-The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have the classical reasoner
-already installed.  We shall first consider how to use it, then see how to
-instantiate it for new logics.
+We shall first discuss the underlying principles, then consider how to use
+the classical reasoner.  Finally, we shall see how to instantiate it for
+new logics.  The logics {\tt FOL}, {\tt HOL} and {\tt ZF} have it already
+installed.
 
 
 \section{The sequent calculus}
@@ -136,7 +137,7 @@
 simulates $({\disj}R)$:
 \[ (\neg Q\Imp P) \Imp P\disj Q \]
 The destruction rule $({\imp}E)$ is replaced by
-\[ \List{P\imp Q;\; \neg P\imp R;\; Q\imp R} \Imp R. \]
+\[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \]
 Quantifier replication also requires special rules.  In classical logic,
 $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules
 $(\exists R)$ and $(\forall L)$ are dual:
@@ -165,7 +166,7 @@
 $$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q.
    \eqno(\forall E@3) $$
 To replicate existential quantifiers, replace $(\exists I)$ by
-\[ \Bigl(\neg(\exists x{.}P(x)) \Imp P(t)\Bigr) \Imp \exists x{.}P(x). \]
+\[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \]
 All introduction rules mentioned above are also useful in swapped form.
 
 Replication makes the search space infinite; we must apply the rules with
@@ -263,6 +264,25 @@
 If installed, the classical module provides several tactics (and other
 operations) for simulating the classical sequent calculus.
 
+\subsection{The automatic tactics}
+\begin{ttbox} 
+fast_tac : claset -> int -> tactic
+best_tac : claset -> int -> tactic
+\end{ttbox}
+Both of these tactics work by applying {\tt step_tac} repeatedly.  Their
+effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
+solve this subgoal or fail.
+\begin{ttdescription}
+\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
+depth-first search, to solve subgoal~$i$.
+
+\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
+best-first search, to solve subgoal~$i$.  A heuristic function ---
+typically, the total size of the proof state --- guides the search.  This
+function is supplied when the classical reasoner is set up.
+\end{ttdescription}
+
+
 \subsection{Single-step tactics}
 \begin{ttbox} 
 safe_step_tac : claset -> int -> tactic
@@ -286,7 +306,7 @@
 \item[\ttindexbold{inst_step_tac} $cs$ $i$] is like {\tt safe_step_tac},
 but allows unknowns to be instantiated.
 
-\item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}.  IF this
+\item[\ttindexbold{step_tac} $cs$ $i$] tries {\tt safe_tac}.  If this
 fails, it tries {\tt inst_step_tac}, or applies an unsafe rule from~$cs$.
 This is the basic step of the proof procedure.
 
@@ -299,25 +319,6 @@
 \end{ttdescription}
 
 
-\subsection{The automatic tactics}
-\begin{ttbox} 
-fast_tac : claset -> int -> tactic
-best_tac : claset -> int -> tactic
-\end{ttbox}
-Both of these tactics work by applying {\tt step_tac} repeatedly.  Their
-effect is restricted (by {\tt SELECT_GOAL}) to one subgoal; they either
-solve this subgoal or fail.
-\begin{ttdescription}
-\item[\ttindexbold{fast_tac} $cs$ $i$] applies {\tt step_tac} using
-depth-first search, to solve subgoal~$i$.
-
-\item[\ttindexbold{best_tac} $cs$ $i$] applies {\tt step_tac} using
-best-first search, to solve subgoal~$i$.  A heuristic function ---
-typically, the total size of the proof state --- guides the search.  This
-function is supplied when the classical reasoner is set up.
-\end{ttdescription}
-
-
 \subsection{Other useful tactics}
 \index{tactics!for contradiction}
 \index{tactics!for Modus Ponens}

--- a/doc-src/Ref/defining.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/defining.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -117,7 +117,8 @@
 \index{*PROP symbol}
 \index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
 \index{*:: symbol}\index{*=> symbol}
-%index command: percent is permitted, but braces must match!
+\index{sort constraints}
+%the index command: a percent is permitted, but braces must match!
 \index{%@{\tt\%} symbol}
 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
 \index{*[ symbol}\index{*] symbol}
@@ -164,6 +165,7 @@
   treating {\tt y} like a type constructor applied to {\tt nat}.  The
   likely result is an error message.  To avoid this interpretation, use
   parentheses and write \verb|(x::nat) y|.
+  \index{type constraints}\index{*:: symbol}
 
   Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
   yields an error.  The correct form is \verb|(x::nat) (y::nat)|.
@@ -295,7 +297,7 @@
 {\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
 \end{ttbox}
 
-As you can see, the output is divided into labeled sections.  The grammar
+As you can see, the output is divided into labelled sections.  The grammar
 is represented by {\tt lexicon}, {\tt roots} and {\tt prods}.  The rest
 refers to syntactic translations and macro expansion.  Here is an
 explanation of the various sections.
@@ -378,7 +380,7 @@
 first-order logic, type~$i$ stands for terms and~$o$ for formulae.  Only
 the outermost type constructor is taken into account.  For example, any
 type of the form $\sigma list$ stands for a list;  productions may refer
-to the symbol {\tt list} and will apply lists of any type.
+to the symbol {\tt list} and will apply to lists of any type.
 
 The symbol associated with a type is called its {\bf root} since it may
 serve as the root of a parse tree.  Precisely, the root of $(\tau@1, \dots,
@@ -411,7 +413,7 @@
 \begin{center}
   {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)}
 \end{center}
-This constant declaration and mixfix annotation is interpreted as follows:
+This constant declaration and mixfix annotation are interpreted as follows:
 \begin{itemize}\index{productions}
 \item The string {\tt $c$} is the name of the constant associated with the
   production; unless it is a valid identifier, it must be enclosed in
@@ -488,7 +490,7 @@
 end
 \end{ttbox}
 The {\tt arities} declaration causes {\tt exp} to be added as a new root.
-If you put this into a file {\tt exp.thy} and load it via {\tt
+If you put this into a file {\tt EXP.thy} and load it via {\tt
   use_thy "EXP"}, you can run some tests:
 \begin{ttbox}
 val read_exp = Syntax.test_read (syn_of EXP.thy) "exp";
@@ -607,6 +609,7 @@
 "\(\Q\)"\hskip-3pt  :: "[idts, \(\tau@2\)] => \(\tau@3\)"   ("(3\(\Q\)_./ _)" \(p\))
 \end{ttbox}
 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
+\index{type constraints}
 optional type constraints (see Fig.\ts\ref{fig:pure_gram}).  The
 declaration also installs a parse translation\index{translations!parse}
 for~$\Q$ and a print translation\index{translations!print} for~$c$ to
@@ -657,7 +660,7 @@
 end
 \end{ttbox}
 The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
-coercion function.  Assuming this definition resides in a file {\tt base.thy},
+coercion function.  Assuming this definition resides in a file {\tt Base.thy},
 you have to load it with the command {\tt use_thy "Base"}.
 
 One of the simplest nontrivial logics is {\bf minimal logic} of
@@ -673,7 +676,7 @@
   MP    "[| P --> Q; P |] ==> Q"
 end
 \end{ttbox}
-After loading this definition from the file {\tt hilbert.thy}, you can
+After loading this definition from the file {\tt Hilbert.thy}, you can
 start to prove theorems in the logic:
 \begin{ttbox}
 goal Hilbert.thy "P --> P";

--- a/doc-src/Ref/goals.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/goals.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -44,7 +44,7 @@
 this list is non-empty, bind its value to an \ML{} identifier by typing
 something like
 \begin{ttbox} 
-val prems = it;
+val prems = goal{\it theory\/ formula};
 \end{ttbox}\index{assumptions!of main goal}
 These assumptions serve as the premises when you are deriving a rule.  They
 are also stored internally and can be retrieved later by the function {\tt
@@ -53,7 +53,7 @@
 
 \index{definitions!unfolding}
 Some of the commands unfold definitions using meta-rewrite rules.  This
-expansion affects both the first subgoal and the premises, which would
+expansion affects both the initial subgoal and the premises, which would
 otherwise require use of {\tt rewrite_goals_tac} and
 {\tt rewrite_rule}.
 
@@ -321,8 +321,8 @@
 
 \item[\ttindexbold{ren} {\it names} {\it i};] 
 performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames
-parameters in subgoal~$i$.  (Ignore the message {\tt Warning:\ same as
-previous level}.)
+parameters in subgoal~$i$.  (Ignore the message {\footnotesize\tt Warning:\
+  same as previous level}.)
 \index{parameters!renaming}
 \end{ttdescription}
 
@@ -341,9 +341,9 @@
 are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}.
 
 The tactic is specified by a function from theorem lists to tactic lists.
-The function is applied to the list of meta-hypotheses taken from the main
-goal.  The resulting tactics are applied in sequence (using {\tt EVERY}).
-For example, a proof consisting of the commands
+The function is applied to the list of meta-assumptions taken from
+the main goal.  The resulting tactics are applied in sequence (using {\tt
+  EVERY}).  For example, a proof consisting of the commands
 \begin{ttbox} 
 val prems = goal {\it theory} {\it formula};
 by \(tac@1\);  \ldots  by \(tac@n\);
@@ -355,17 +355,10 @@
  (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
 \end{ttbox}
 The methods perform identical processing of the initial {\it formula} and
-the final proof state, but {\tt prove_goal} executes the tactic as a
-atomic operation, bypassing the subgoal module.  
-
-A batch proof may alternatively consist of subgoal commands encapsulated
-using~{\tt let}:
-\begin{ttbox} 
-val my_thm = 
-    let val prems = goal {\it theory} {\it formula}
-    in  by \(tac@1\);  \ldots  by \(tac@n\);  result() end;
-\end{ttbox}
-
+the final proof state.  But {\tt prove_goal} executes the tactic as a
+atomic operation, bypassing the subgoal module; the current interactive
+proof is unaffected.
+%
 \begin{ttdescription}
 \item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] 
 executes a proof of the {\it formula\/} in the given {\it theory}, using
@@ -429,7 +422,7 @@
 
 \item[\ttindexbold{pop_proof}();]  
 discards the top element of the stack.  It returns the list of
-meta-hypotheses associated with the new proof;  you should bind these to an
+assumptions associated with the new proof;  you should bind these to an
 \ML\ identifier.  They can also be obtained by calling \ttindex{premises}.
 
 \item[\ttindexbold{rotate_proof}();]

--- a/doc-src/Ref/introduction.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/introduction.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -142,7 +142,7 @@
 
 \begin{ttdescription}
 \item[\ttindexbold{show_hyps} := false;]   
-makes Isabelle show each meta-level hypotheses as a dot.
+makes Isabelle show each meta-level hypothesis as a dot.
 
 \item[\ttindexbold{show_types} := true;]
 makes Isabelle show types when printing a term or theorem.
@@ -160,7 +160,7 @@
 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
 provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
-unification occasionally puts terms into a fully $\eta$-expanded form.  For
+unification frequently puts terms into a fully $\eta$-expanded form.  For
 example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
 $\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
 form.

--- a/doc-src/Ref/simplifier.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/simplifier.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -19,7 +19,8 @@
 Experienced users can exploit the other components to streamline proofs.
 
 
-\subsection{Rewrite rules}\index{rewrite rules}
+\subsection{Rewrite rules}
+\index{rewrite rules|(}
 Rewrite rules are theorems expressing some form of equality:
 \begin{eqnarray*}
   Suc(\Var{m}) + \Var{n} &=&      \Var{m} + Suc(\Var{n}) \\
@@ -41,18 +42,22 @@
 local assumptions.
 
 
-\begin{warn}\index{rewrite rules}
+\begin{warn}
   The left-hand side of a rewrite rule must look like a first-order term:
-  after eta-contraction, none of its unknowns should have arguments.  Hence
-  ${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ and $\neg(\forall
-  x.\Var{P}(x)) \bimp (\exists x.\neg\Var{P}(x))$ are acceptable, whereas
-  $\Var{f}(\Var{x})\in {\tt range}(\Var{f}) = True$ is not.  However, you can
-  replace the offending subterms by new variables and conditions: $\Var{y} =
-  \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$ is again
-  acceptable.
+  none of its unknowns should have arguments.  Hence
+  ${\Var{i}+(\Var{j}+\Var{k})} = {(\Var{i}+\Var{j})+\Var{k}}$ is
+  acceptable.  Even $\neg(\forall x.\Var{P}(x)) \bimp (\exists
+  x.\neg\Var{P}(x))$ is acceptable because its left-hand side is
+  $\neg(All(\Var{P}))$ after $\eta$-contraction.  But ${\Var{f}(\Var{x})\in
+    {\tt range}(\Var{f})} = True$ is not acceptable.  However, you can
+  replace the offending subterms by adding new variables and conditions:
+  $\Var{y} = \Var{f}(\Var{x}) \Imp \Var{y}\in {\tt range}(\Var{f}) = True$
+  is acceptable as a conditional rewrite rule.
 \end{warn}
 
-\subsection {Congruence rules}\index{congruence rules}
+\index{rewrite rules|)}
+
+\subsection{*Congruence rules}\index{congruence rules}
 Congruence rules are meta-equalities of the form
 \[ \List{\dots} \Imp
    f(\Var{x@1},\ldots,\Var{x@n}) \equiv f(\Var{y@1},\ldots,\Var{y@n}).
@@ -108,10 +113,11 @@
 The subgoaler can be set explicitly with \ttindex{setsubgoaler}.  For
 example, the subgoaler
 \begin{ttbox}
-fun subgoal_tac ss = resolve_tac (prems_of_ss ss) ORELSE' 
+fun subgoal_tac ss = assume_tac ORELSE'
+                     resolve_tac (prems_of_ss ss) ORELSE' 
                      asm_simp_tac ss;
 \end{ttbox}
-tries to solve the subgoal with one of the premises and calls
+tries to solve the subgoal by assumption or with one of the premises, calling
 simplification only if that fails; here {\tt prems_of_ss} extracts the
 current premises from a simpset.
 
@@ -229,9 +235,10 @@
   is like \verb$simp_tac$, but extracts additional rewrite rules from the
   assumptions.
 
-\item[\ttindexbold{asm_full_simp_tac}] is like \verb$asm_simp_tac$, but also
-  simplifies the assumptions one by one, using each assumption in the
-  simplification of the following ones.
+\item[\ttindexbold{asm_full_simp_tac}] 
+  is like \verb$asm_simp_tac$, but also simplifies the assumptions one by
+  one.  Working from left to right, it uses each assumption in the
+  simplification of those following.
 \end{ttdescription}
 Using the simplifier effectively may take a bit of experimentation.  The
 tactics can be traced with the ML command \verb$trace_simp := true$.  To
@@ -253,7 +260,7 @@
     \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$.
 \item[FOL_ss]
   is a basic simpset for {\tt FOL}.%
-\footnote{These examples reside on the file {\tt FOL/ex/nat.ML}.} 
+\footnote{These examples reside on the file {\tt FOL/ex/Nat.ML}.} 
 \end{ttdescription}
 
 We create a simpset for natural numbers by extending~{\tt FOL_ss}:
@@ -397,7 +404,7 @@
 \end{ttbox}
 
 
-\section{*Permutative rewrite rules}
+\section{Permutative rewrite rules}
 \index{rewrite rules!permutative|(}
 
 A rewrite rule is {\bf permutative} if the left-hand side and right-hand
@@ -455,7 +462,7 @@
        sum_Suc    "sum(f,Suc(n)) = f(n) + sum(f,n)"
 end
 \end{ttbox}
-After declaring {\tt open Natsum}, we make the required simpset by adding
+After declaring {\tt open NatSum}, we make the required simpset by adding
 the AC-rules for~$+$ and the axioms for~{\tt sum}:
 \begin{ttbox}
 val natsum_ss = arith_ss addsimps ([sum_0,sum_Suc] \at add_ac);
@@ -564,7 +571,7 @@
 Of course, you should only assert such rules if they are true for your
 particular logic.  In Constructive Type Theory, equality is a ternary
 relation of the form $a=b\in A$; the type~$A$ determines the meaning of the
-equality effectively as a partial equivalence relation.  The present
+equality essentially as a partial equivalence relation.  The present
 simplifier cannot be used.  Rewriting in {\tt CTT} uses another simplifier,
 which resides in the file {\tt typedsimp.ML} and is not documented.  Even
 this does not work for later variants of Constructive Type Theory that use

--- a/doc-src/Ref/substitution.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/substitution.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -3,19 +3,18 @@
 \index{tactics!substitution|(}\index{equality|(}
 
 Replacing equals by equals is a basic form of reasoning.  Isabelle supports
-several kinds of equality reasoning.  {\bf Substitution} means to replace
+several kinds of equality reasoning.  {\bf Substitution} means replacing
 free occurrences of~$t$ by~$u$ in a subgoal.  This is easily done, given an
-equality $t=u$, provided the logic possesses the appropriate rule ---
-unless you want to substitute even in the assumptions.  The tactic
-{\tt hyp_subst_tac} performs substitution in the assumptions, but it
-works via object-level implication, and therefore must be specially set up
-for each suitable object-logic.
+equality $t=u$, provided the logic possesses the appropriate rule.  The
+tactic {\tt hyp_subst_tac} performs substitution even in the assumptions.
+But it works via object-level implication, and therefore must be specially
+set up for each suitable object-logic.
 
 Substitution should not be confused with object-level {\bf rewriting}.
 Given equalities of the form $t=u$, rewriting replaces instances of~$t$ by
 corresponding instances of~$u$, and continues until it reaches a normal
 form.  Substitution handles `one-off' replacements by particular
-equalities, while rewriting handles general equalities.
+equalities while rewriting handles general equations.
 Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics.
 
 
@@ -35,12 +34,12 @@
 the first unifier includes all the occurrences.}  To replace $u$ by~$t$ in
 subgoal~$i$, use
 \begin{ttbox} 
-resolve_tac [eqth RS subst] \(i\) {\it.}
+resolve_tac [eqth RS subst] \(i\){\it.}
 \end{ttbox}
 To replace $t$ by~$u$ in
 subgoal~$i$, use
 \begin{ttbox} 
-resolve_tac [eqth RS ssubst] \(i\) {\it,}
+resolve_tac [eqth RS ssubst] \(i\){\it,}
 \end{ttbox}
 where \tdxbold{ssubst} is the `swapped' substitution rule
 $$ \List{\Var{a}=\Var{b}; \Var{P}(\Var{b})} \Imp 
@@ -55,7 +54,7 @@
 Elim-resolution is well-behaved with assumptions of the form $t=u$.
 To replace $u$ by~$t$ or $t$ by~$u$ in subgoal~$i$, use
 \begin{ttbox} 
-eresolve_tac [subst] \(i\)    {\it or}    eresolve_tac [ssubst] \(i\) {\it.}
+eresolve_tac [subst] \(i\)    {\rm or}    eresolve_tac [ssubst] \(i\){\it.}
 \end{ttbox}
 
 
@@ -93,7 +92,7 @@
 contradict a theorem that states $0\not=1$, rather than to replace 0 by~1
 in the subgoal!
 
-Replacing a free variable causes similar problems if they appear in the
+Substitution for free variables is also unhelpful if they appear in the
 premises of a rule being derived --- the substitution affects object-level
 assumptions, not meta-level assumptions.  For instance, replacing~$a$
 by~$b$ could make the premise~$P(a)$ worthless.  To avoid this problem, use
@@ -153,7 +152,7 @@
 Here {\tt Trueprop} is the coercion from type~$o$ to type~$prop$, while
 \hbox{\tt op =} is the internal name of the infix operator~{\tt=}.
 Pattern-matching expresses the function concisely, using wildcards~({\tt_})
-to hide the types.
+for the types.
 
 Here is how {\tt hyp_subst_tac} works.  Given a subgoal of the form
 \[ \List{P@1; \cdots ; t=u; \cdots ; P@n} \Imp Q, \] it locates a suitable

--- a/doc-src/Ref/syntax.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/syntax.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -64,7 +64,7 @@
 %
 Isabelle uses an S-expression syntax for abstract syntax trees.  Constant
 atoms are shown as quoted strings, variable atoms as non-quoted strings and
-applications as a parenthesized list of subtrees.  For example, the \AST
+applications as a parenthesised list of subtrees.  For example, the \AST
 \begin{ttbox}
 Appl [Constant "_constrain",
       Appl [Constant "_abs", Variable "x", Variable "t"],
@@ -270,11 +270,11 @@
     \]
 \end{itemize}
 %
-Type constraints are inserted to allow the printing of types.  This is
-governed by the boolean variable \ttindex{show_types}:
+Type constraints\index{type constraints} are inserted to allow the printing
+of types.  This is governed by the boolean variable \ttindex{show_types}:
 \begin{itemize}
   \item $constrain(x, \tau) = x$ \ if $\tau = \mtt{dummyT}$ \index{*dummyT} or
-    \ttindex{show_types} not set to {\tt true}.
+    \ttindex{show_types} is set to {\tt false}.
 
   \item $constrain(x, \tau) = \Appl{\Constant \mtt{"_constrain"}, x, 
          \astofterm{\tau}}$ \ otherwise.  
@@ -289,7 +289,7 @@
 %
 The \AST{}, after application of macros (see \S\ref{sec:macros}), is
 transformed into the final output string.  The built-in {\bf print AST
-  translations}\indexbold{translations!print AST} effectively reverse the
+  translations}\indexbold{translations!print AST} reverse the
 parse \AST{} translations of Fig.\ts\ref{fig:parse_ast_tr}.
 
 For the actual printing process, the names attached to productions
@@ -338,11 +338,11 @@
 Figure~\ref{fig:set_trans} defines a fragment of first-order logic and set
 theory.\footnote{This and the following theories are complete working
   examples, though they specify only syntax, no axioms.  The file {\tt
-    ZF/zf.thy} presents the full set theory definition, including many
+    ZF/ZF.thy} presents the full set theory definition, including many
   macro rules.}  Theory {\tt SET} defines constants for set comprehension
 ({\tt Collect}), replacement ({\tt Replace}) and bounded universal
 quantification ({\tt Ball}).  Each of these binds some variables.  Without
-additional syntax we should have to express $\forall x \in A.  P$ as {\tt
+additional syntax we should have to write $\forall x \in A.  P$ as {\tt
   Ball(A,\%x.P)}, and similarly for the others.
 
 \begin{figure}
@@ -464,7 +464,7 @@
 If \ttindex{eta_contract} is set to {\tt true}, terms will be
 $\eta$-contracted {\em before\/} the \AST{} rewriter sees them.  Thus some
 abstraction nodes needed for print rules to match may vanish.  For example,
-\verb|Ball(A, %x. P(x))| contracts {\tt Ball(A, P)}; the print rule does
+\verb|Ball(A, %x. P(x))| contracts to {\tt Ball(A, P)}; the print rule does
 not apply and the output will be {\tt Ball(A, P)}.  This problem would not
 occur if \ML{} translation functions were used instead of macros (as is
 done for binder declarations).
@@ -491,10 +491,10 @@
 \subsection{Applying rules}
 As a term is being parsed or printed, an \AST{} is generated as an
 intermediate form (recall Fig.\ts\ref{fig:parse_print}).  The \AST{} is
-normalized by applying macro rules in the manner of a traditional term
+normalised by applying macro rules in the manner of a traditional term
 rewriting system.  We first examine how a single rule is applied.
 
-Let $t$ be the abstract syntax tree to be normalized and $(l, r)$ some
+Let $t$ be the abstract syntax tree to be normalised and $(l, r)$ some
 translation rule.  A subtree~$u$ of $t$ is a {\bf redex} if it is an
 instance of~$l$; in this case $l$ is said to {\bf match}~$u$.  A redex
 matched by $l$ may be replaced by the corresponding instance of~$r$, thus
@@ -546,10 +546,10 @@
 \end{ttbox}
 The term {\tt Nil} will be printed as {\tt []}, just as expected.
 The term \verb|%Nil.t| will be printed as \verb|%[].t|, which might not be
-expected! 
+expected!  How is the type~{\tt Nil} printed?
 
 Normalizing an \AST{} involves repeatedly applying macro rules until none
-is applicable.  Macro rules are chosen in the order that they appear in the
+are applicable.  Macro rules are chosen in the order that they appear in the
 {\tt translations} section.  You can watch the normalization of \AST{}s
 during parsing and printing by setting \ttindex{Syntax.trace_norm_ast} to
 {\tt true}.\index{tracing!of macros} Alternatively, use
@@ -626,7 +626,7 @@
 The parse rules only work in the order given.
 
 \begin{warn}
-  The \AST{} rewriter cannot discern constants from variables and looks
+  The \AST{} rewriter cannot distinguish constants from variables and looks
   only for names of atoms.  Thus the names of {\tt Constant}s occurring in
   the (internal) left-hand side of translation rules should be regarded as
   \rmindex{reserved words}.  Choose non-identifiers like {\tt\at Finset} or
@@ -635,7 +635,7 @@
 \begin{ttbox}
 \%empty insert. insert(x, empty)
 \end{ttbox}
-  gets printed as \verb|%empty insert. {x}|.
+\par\noindent is printed as \verb|%empty insert. {x}|.
 \end{warn}
 
 
@@ -690,8 +690,8 @@
 This section describes the translation function mechanism.  By writing
 \ML{} functions, you can do almost everything with terms or \AST{}s during
 parsing and printing.  The logic \LK\ is a good example of sophisticated
-transformations between internal and external representations of
-associative sequences; here, macros would be useless.
+transformations between internal and external representations of sequents;
+here, macros would be useless. 
 
 A full understanding of translations requires some familiarity
 with Isabelle's internals, especially the datatypes {\tt term}, {\tt typ},
@@ -805,9 +805,10 @@
       else list_comb (Const (r, dummyT) $ A $ B, ts)
   | dependent_tr' _ _ = raise Match;
 \end{ttbox}
-The argument {\tt (q,r)} is supplied to {\tt dependent_tr'} by a curried
-function application during its installation.  We could set up print
-translations for both {\tt Pi} and {\tt Sigma} by including
+The argument {\tt (q,r)} is supplied to the curried function {\tt
+  dependent_tr'} by a partial application during its installation.  We
+can set up print translations for both {\tt Pi} and {\tt Sigma} by
+including
 \begin{ttbox}\index{*ML section}
 val print_translation =
   [("Pi",    dependent_tr' ("{\at}PROD", "{\at}->")),
@@ -815,11 +816,11 @@
 \end{ttbox}
 within the {\tt ML} section.  The first of these transforms ${\tt Pi}(A,
 \mtt{Abs}(x, T, B))$ into $\hbox{\tt{\at}PROD}(x', A, B')$ or
-$\hbox{\tt{\at}->}r(A, B)$, choosing the latter form if $B$ does not depend
+$\hbox{\tt{\at}->}(A, B)$, choosing the latter form if $B$ does not depend
 on~$x$.  It checks this using \ttindex{loose_bnos}, yet another function
 from {\tt Pure/term.ML}.  Note that $x'$ is a version of $x$ renamed away
-from all names in $B$, and $B'$ the body $B$ with {\tt Bound} nodes
-referring to our {\tt Abs} node replaced by $\ttfct{Free} (x',
+from all names in $B$, and $B'$ is the body $B$ with {\tt Bound} nodes
+referring to the {\tt Abs} node replaced by $\ttfct{Free} (x',
 \mtt{dummyT})$.
 
 We must be careful with types here.  While types of {\tt Const}s are

--- a/doc-src/Ref/tactic.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/tactic.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -109,19 +109,20 @@
 \end{ttbox}
 These tactics are designed for applying rules such as substitution and
 induction, which cause difficulties for higher-order unification.  The
-tactics accept explicit instantiations for schematic variables in the rule
---- typically, in the rule's conclusion.  Each instantiation is a pair
-{\tt($v$,$e$)}, where $v$ can be a type variable or ordinary variable:
+tactics accept explicit instantiations for unknowns in the rule ---
+typically, in the rule's conclusion.  Each instantiation is a pair
+{\tt($v$,$e$)}, where $v$ is an unknown {\em without\/} its leading
+question mark!
 \begin{itemize}
-\item If $v$ is the {\bf type variable} {\tt'a}, then
-the rule must contain a schematic type variable \verb$?'a$ of some
+\item If $v$ is the type unknown {\tt'a}, then
+the rule must contain a type unknown \verb$?'a$ of some
 sort~$s$, and $e$ should be a type of sort $s$.
 
-\item If $v$ is the {\bf variable} {\tt P}, then
-the rule must contain a schematic variable \verb$?P$ of some type~$\tau$,
+\item If $v$ is the unknown {\tt P}, then
+the rule must contain an unknown \verb$?P$ of some type~$\tau$,
 and $e$ should be a term of some type~$\sigma$ such that $\tau$ and
 $\sigma$ are unifiable.  If the unification of $\tau$ and $\sigma$
-instantiates any schematic type variables in $\tau$, these instantiations
+instantiates any type unknowns in $\tau$, these instantiations
 are recorded for application to the rule.
 \end{itemize}
 Types are instantiated before terms.  Because type instantiations are
@@ -142,7 +143,7 @@
 instantiates the rule {\it thm} with the instantiations {\it insts}, as
 described above, and then performs resolution on subgoal~$i$.  Resolution
 typically causes further instantiations; you need not give explicit
-instantiations for every variable in the rule.
+instantiations for every unknown in the rule.
 
 \item[\ttindexbold{eres_inst_tac}] 
 is like {\tt res_inst_tac}, but performs elim-resolution.
@@ -162,17 +163,17 @@
 \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold}
 \index{definitions}
 
-Definitions in Isabelle have the form $t\equiv u$, where typically $t$ is a
+Definitions in Isabelle have the form $t\equiv u$, where $t$ is typically a
 constant or a constant applied to a list of variables, for example $\it
 sqr(n)\equiv n\times n$.  (Conditional definitions, $\phi\Imp t\equiv u$,
-are not supported.)  {\bf Unfolding} the definition $t\equiv u$ means using
+are not supported.)  {\bf Unfolding} the definition ${t\equiv u}$ means using
 it as a rewrite rule, replacing~$t$ by~$u$ throughout a theorem.  {\bf
 Folding} $t\equiv u$ means replacing~$u$ by~$t$.  Rewriting continues until
 no rewrites are applicable to any subterm.
 
 There are rules for unfolding and folding definitions; Isabelle does not do
 this automatically.  The corresponding tactics rewrite the proof state,
-yielding a unique result.  See also the {\tt goalw} command, which is the
+yielding a single next state.  See also the {\tt goalw} command, which is the
 easiest way of handling definitions.
 \begin{ttbox} 
 rewrite_goals_tac : thm list -> tactic
@@ -204,12 +205,12 @@
 \index{tactics!resolution}\index{tactics!assumption}
 \index{tactics!meta-rewriting}
 \begin{ttbox} 
-rtac     : thm -> int ->tactic
-etac     : thm -> int ->tactic
-dtac     : thm -> int ->tactic
-atac     : int ->tactic
+rtac     :      thm -> int -> tactic
+etac     :      thm -> int -> tactic
+dtac     :      thm -> int -> tactic
+atac     :             int -> tactic
 ares_tac : thm list -> int -> tactic
-rewtac   : thm -> tactic
+rewtac   :      thm ->        tactic
 \end{ttbox}
 These abbreviate common uses of tactics.
 \begin{ttdescription}
@@ -224,7 +225,7 @@
 destruct-resolution.
 
 \item[\ttindexbold{atac} {\it i}] 
-is a synonym for \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
+abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
 
 \item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
 tries proof by assumption and resolution; it abbreviates
@@ -244,8 +245,7 @@
 cut_inst_tac  : (string*string)list -> thm -> int -> tactic
 subgoal_tac   : string -> int -> tactic
 \end{ttbox}
-These tactics add assumptions --- which must be proved, sooner or later ---
-to a given subgoal.
+These tactics add assumptions to a given subgoal.
 \begin{ttdescription}
 \item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
   adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have
@@ -367,7 +367,7 @@
 \begin{ttbox}
 compose_tac: (bool * thm * int) -> int -> tactic
 \end{ttbox}
-{\bf Composing} two rules means to resolve them without prior lifting or
+{\bf Composing} two rules means resolving them without prior lifting or
 renaming of unknowns.  This low-level operation, which underlies the
 resolution tactics, may occasionally be useful for special effects.
 A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
@@ -422,7 +422,7 @@
 \item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
 returns the result of 
 \begin{ttbox}
-subgoals_of_brl {\it brl1} < subgoals_of_brl {\it brl2}
+subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
 \end{ttbox}
 \end{ttdescription}
 Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
@@ -463,7 +463,7 @@
 several functions for `compiling' long lists of rules into fast
 resolution tactics.  When supplied with a list of theorems, these functions
 build a discrimination net; the net is used when the tactic is applied to a
-goal.  To avoid repreatedly constructing the nets, use currying: bind the
+goal.  To avoid repeatedly constructing the nets, use currying: bind the
 resulting tactics to \ML{} identifiers.
 
 \begin{ttdescription}
@@ -562,15 +562,15 @@
 pause_tac: tactic
 print_tac: tactic
 \end{ttbox}
-These violate the functional behaviour of tactics by printing information
-when they are applied to a proof state.  Their output may be difficult to
-interpret.  Note that certain of the searching tacticals, such as {\tt
-REPEAT}, have built-in tracing options.
+These tactics print tracing information when they are applied to a proof
+state.  Their output may be difficult to interpret.  Note that certain of
+the searching tacticals, such as {\tt REPEAT}, have built-in tracing
+options.
 \begin{ttdescription}
 \item[\ttindexbold{pause_tac}] 
-prints {\tt** Press RETURN to continue:} and then reads a line from the
-terminal.  If this line is blank then it returns the proof state unchanged;
-otherwise it fails (which may terminate a repetition).
+prints {\footnotesize\tt** Press RETURN to continue:} and then reads a line
+from the terminal.  If this line is blank then it returns the proof state
+unchanged; otherwise it fails (which may terminate a repetition).
 
 \item[\ttindexbold{print_tac}] 
 returns the proof state unchanged, with the side effect of printing it at
@@ -612,7 +612,7 @@
 \item[Sequence.pull $s$] 
 returns {\tt None} if the sequence is empty and {\tt Some($x$,$s'$)} if the
 sequence has head~$x$ and tail~$s'$.  Warning: calling \hbox{Sequence.pull
-$s$} again will {\bf recompute} the value of~$x$; it is not stored!
+$s$} again will {\it recompute\/} the value of~$x$; it is not stored!
 \end{ttdescription}
 
 
@@ -623,7 +623,7 @@
 s_of_list : 'a list -> 'a seq
 \end{ttbox}
 \begin{ttdescription}
-\item[Sequence.chop ($n$, $s$)] 
+\item[Sequence.chop($n$,$s$)] 
 returns the first~$n$ elements of~$s$ as a list, paired with the remaining
 elements of~$s$.  If $s$ has fewer than~$n$ elements, then so will the
 list.
@@ -645,10 +645,10 @@
 filters    : ('a -> bool) -> 'a seq -> 'a seq
 \end{ttbox} 
 \begin{ttdescription}
-\item[Sequence.append ($s@1$, $s@2$)] 
+\item[Sequence.append($s@1$,$s@2$)] 
 concatenates $s@1$ to $s@2$.
 
-\item[Sequence.interleave ($s@1$, $s@2$)] 
+\item[Sequence.interleave($s@1$,$s@2$)] 
 joins $s@1$ with $s@2$ by interleaving their elements.  The result contains
 all the elements of the sequences, even if both are infinite.
 

--- a/doc-src/Ref/tctical.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/tctical.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -139,7 +139,7 @@
 Note {\tt REPEAT}'s explicit abstraction over the proof state.  Recursive
 tacticals must be coded in this awkward fashion to avoid infinite
 recursion.  With the following definition, \hbox{\tt REPEAT $tac$} would
-loop:
+loop due to \ML's eager evaluation strategy:
 \begin{ttbox} 
 fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
 \end{ttbox}
@@ -185,8 +185,8 @@
 \index{tracing!of searching tacticals}
 \begin{ttbox} 
 DEPTH_FIRST   : (thm->bool) -> tactic -> tactic
-DEPTH_SOLVE   : tactic -> tactic
-DEPTH_SOLVE_1 : tactic -> tactic
+DEPTH_SOLVE   :                tactic -> tactic
+DEPTH_SOLVE_1 :                tactic -> tactic
 trace_DEPTH_FIRST: bool ref \hfill{\bf initially false}
 \end{ttbox}
 \begin{ttdescription}
@@ -213,7 +213,7 @@
 \index{tacticals!searching}
 \index{tracing!of searching tacticals}
 \begin{ttbox} 
-BREADTH_FIRST   : (thm->bool) -> tactic -> tactic
+BREADTH_FIRST   :            (thm->bool) -> tactic -> tactic
 BEST_FIRST      : (thm->bool)*(thm->int) -> tactic -> tactic
 THEN_BEST_FIRST : tactic * ((thm->bool) * (thm->int) * tactic)
                   -> tactic                    \hfill{\bf infix 1}
@@ -330,11 +330,11 @@
 \hbox{\tt SELECT_GOAL {\it tac} $i$}.
 
 {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$,
-with the one subgoal~$\phi$.  If subgoal~$i$ has the form then
-$(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact $\List{\psi\Imp\theta;\;
-  \psi}\Imp\theta$, a proof state with two subgoals.  Such a proof state
-might cause tactics to go astray.  Therefore {\tt SELECT_GOAL} inserts a
-quantifier to create the state
+with the one subgoal~$\phi$.  If subgoal~$i$ has the form $\psi\Imp\theta$
+then $(\psi\Imp\theta)\Imp(\psi\Imp\theta)$ is in fact
+$\List{\psi\Imp\theta;\; \psi}\Imp\theta$, a proof state with two subgoals.
+Such a proof state might cause tactics to go astray.  Therefore {\tt
+  SELECT_GOAL} inserts a quantifier to create the state
 \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \]
 
 \item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions}
@@ -362,6 +362,8 @@
 \begin{ttbox} 
 val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1);
 \end{ttbox} 
+The function \ttindex{gethyps} is useful for debugging applications of {\tt
+  METAHYPS}. 
 \end{ttdescription}
 
 \begin{warn}

--- a/doc-src/Ref/theories.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/theories.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -10,8 +10,8 @@
 returning a message and a list of theories.
 
 Signatures, which contain information about sorts, types, constants and
-syntax, have the \ML\ type~\mltydx{Sign.sg}.  For identification,
-each signature carries a unique list of {\bf stamps}, which are \ML\
+syntax, have the \ML\ type~\mltydx{Sign.sg}.  For identification, each
+signature carries a unique list of \bfindex{stamps}, which are \ML\ 
 references to strings.  The strings serve as human-readable names; the
 references serve as unique identifiers.  Each primitive signature has a
 single stamp.  When two signatures are merged, their lists of stamps are
@@ -68,7 +68,7 @@
   Only 2-place type constructors can have infix status and symbolic names;
   an example is {\tt ('a,'b)"*"}, which expresses binary product types.
 
-  A {\bf type synonym}\indexbold{types!synonyms} is an abbreviation
+  A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
   $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where
   $name$ can be a string and $\tau$ must be enclosed in quotation marks.
   
@@ -177,41 +177,37 @@
 \end{ttdescription}
 %
 Each theory definition must reside in a separate file.  Let the file {\it
-  tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
-theories $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it
-  TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes a temporary \ML{}
-file {\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file.  Recursive {\tt
+  T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
+theories are $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"{\it
+  T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
+file {\tt.{\it T}.thy.ML}, and reads the latter file.  Recursive {\tt
   use_thy} calls load those parent theories that have not been loaded
-previously; the recursion may continue to any depth.  One {\tt use_thy}
-call can read an entire logic if all theories are linked appropriately.
-
-The result is an \ML\ structure~$TF$ containing a component {\tt thy} for
-the new theory and components $r@1$ \dots $r@n$ for the rules.  The
-structure also contains the definitions of the {\tt ML} section, if
-present.  The file {\tt.}{\it tf}{\tt.thy.ML} is then deleted if
-{\tt delete_tmpfiles} is set to {\tt true} and no errors occurred.
+previously; the recursive calls may continue to any depth.  One {\tt use_thy}
+call can read an entire logic provided all theories are linked appropriately.
 
-Finally the file {\it tf}{\tt.ML} is read, if it exists.  This file
-normally contains proofs involving the new theory.  It is also possible to
-provide only a {\tt.ML} file, with no {\tt.thy} file.  In this case the
-{\tt.ML} file must declare an \ML\ structure having the theory's name.  If
-both the {\tt.thy} file and a structure declaration in the {\tt.ML} file
-exist, then the latter declaration is used.  See {\tt ZF/ex/llist.ML} for
-an example.
+The result is an \ML\ structure~$T$ containing a component {\tt thy} for
+the new theory and components for each of the rules.  The structure also
+contains the definitions of the {\tt ML} section, if present.  The file
+{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set
+to {\tt true} and no errors occurred.
 
-\indexbold{theories!names of}\indexbold{files!names of}
-\begin{warn}
-  Case is significant.  The argument of \ttindex{use_thy} should be the
-  exact theory name, as defined in the theory file.  The corresponding
-  filenames are derived by appending {\tt.thy} or {\tt.ML} to the theory's
-  name {\it after conversion to lower case}.
-\end{warn}
+Finally the file {\it T}{\tt.ML} is read, if it exists.  This file normally
+begins with the declaration {\tt open~$T$} and contains proofs involving
+the new theory.
+
+Special applications, such as \ZF's inductive definition package, construct
+theories directly by calling the \ML{} function {\tt extend_theory}.  In
+this situation there is no {\tt.thy} file, only an {\tt.ML} file.  The
+{\tt.ML} file must declare an \ML\ structure having the theory's name.  See
+the file {\tt ZF/ex/LList.ML} for an example.
+Section~\ref{sec:pseudo-theories} below describes a way of linking such
+theories to their parents.
 
 \begin{warn}
-  Temporary files are written to the current directory, which therefore
-  must be writable.  Isabelle inherits the current directory from the
-  operating system; you can change it within Isabelle by typing
-  \hbox{\tt\ \ \ttindex{cd} "{\it dir}";\ \ }.
+Temporary files are written to the current directory, which therefore must
+be writable.  Isabelle inherits the current directory from the operating
+system; you can change it within Isabelle by typing \hbox{\tt\ \ 
+  \ttindex{cd} "{\it dir}";\ \ }.
 \end{warn}
 
 
@@ -221,6 +217,11 @@
 update     : unit -> unit
 unlink_thy : string -> unit
 \end{ttbox}
+Changing a theory on disk often makes it necessary to reload all theories
+descended from it.  However, {\tt use_thy} reads only one theory, even if
+some of the parent theories are out of date.  In this case you should call
+{\tt update()}.
+
 Isabelle keeps track of all loaded theories and their files.  If
 \ttindex{use_thy} finds that the theory to be loaded has been read before,
 it determines whether to reload the theory as follows.  First it looks for
@@ -229,15 +230,9 @@
 are equal.  If the files have been moved, {\tt use_thy} searches for them
 as it would for a new theory.  After {\tt use_thy} reloads a theory, it
 marks the children as out-of-date.
-\begin{warn}
-  Changing a theory on disk often makes it necessary to reload all theories
-  descended from it.  However, {\tt use_thy} reads only one theory, even if
-  some of the parent theories are out of date.  In this case you should
-  call {\tt update()}.
-\end{warn}
 
 \begin{ttdescription}
-\item[\ttindexbold{update} ()] 
+\item[\ttindexbold{update}()] 
   reloads all modified theories and their descendants in the correct order.  
 
 \item[\ttindexbold{unlink_thy} $thyname$]\indexbold{theories!removing}
@@ -247,6 +242,7 @@
 \end{ttdescription}
 
 
+\goodbreak
 \subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
 The theory mechanism depends upon reference variables.  At the end of a
 Poly/\ML{} session, the contents of references are lost unless they are
@@ -266,13 +262,17 @@
 has no loaded theories, since they allocate new references.
 
 
-\subsection{*Pseudo theories}\indexbold{theories!pseudo}
+\subsection{*Pseudo theories}\label{sec:pseudo-theories}
+\indexbold{theories!pseudo}%
 Any automatic reloading facility requires complete knowledge of all
 dependencies.  Sometimes theories depend on objects created in \ML{} files
-with no associated {\tt.thy} file.  Unless such dependencies are documented,
-{\tt update} fails to reload these \ML{} files and the system is left in a
-state where some objects, such as theorems, still refer to old versions of
-theories.  This may lead to the error
+with no associated {\tt.thy} file.  These objects may be theories but they
+could also be theorems, proof procedures, etc.
+
+Unless such dependencies are documented, {\tt update} fails to reload these
+\ML{} files and the system is left in a state where some objects, such as
+theorems, still refer to old versions of theories.  This may lead to the
+error
 \begin{ttbox}
 Attempt to merge different versions of theory: \(T\)
 \end{ttbox}
@@ -280,8 +280,8 @@
 those without associated {\tt.thy} file.
 
 Let us assume we have an orphaned \ML{} file named {\tt orphan.ML} and a
-theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt b.ML} uses
-theorems proved in {\tt orphan.ML}.  Then {\tt b.thy} should
+theory~$B$ that depends on {\tt orphan.ML} --- for example, {\tt B.ML} uses
+theorems proved in {\tt orphan.ML}.  Then {\tt B.thy} should
 mention this dependence by means of a string:
 \begin{ttbox}
 B = ... + "orphan" + ...
@@ -327,17 +327,17 @@
   complains about additional assumptions, but \ttindex{uresult} does not.
 
 For example, if {\it formula} is
-\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form
-\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]}
+\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
+\hbox{\verb'?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]'}
 \end{ttdescription}
 
 \subsection{Building a theory}
 \label{BuildingATheory}
 \index{theories!constructing|bold}
 \begin{ttbox} 
-pure_thy: theory
-merge_theories: theory * theory -> theory
-extend_theory: theory -> string -> \(\cdots\) -> theory
+pure_thy       : theory
+merge_theories : theory * theory -> theory
+extend_theory  : theory -> string -> \(\cdots\) -> theory
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
@@ -414,7 +414,7 @@
 \hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.
 
 \item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
-returns the stamps of the signature associated with~$thy$.
+returns the \rmindex{stamps} of the signature associated with~$thy$.
 
 \item[\ttindexbold{sign_of} $thy$] 
 returns the signature associated with~$thy$.  It is useful with functions
@@ -470,7 +470,7 @@
 is the {\bf application} of~$t$ to~$u$.  
 \end{ttdescription}
 Application is written as an infix operator to aid readability.
-Here is an \ML\ pattern to recognize first-order formulae of
+Here is an \ML\ pattern to recognize \FOL{} formulae of
 the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
 \begin{ttbox} 
 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
@@ -496,7 +496,7 @@
   the number 0.  A well-formed term does not contain any loose variables.
 
 \item[\ttindexbold{incr_boundvars} $j$] 
-  increases a term's dangling bound variables by the offset~$j$.  This
+  increases a term's dangling bound variables by the offset~$j$.  This is
   required when moving a subterm into a context where it is enclosed by a
   different number of abstractions.  Bound variables with a matching
   abstraction are unaffected.
@@ -510,7 +510,7 @@
   substitutes into $u$, which should be the body of an abstraction.
   It replaces each occurrence of the outermost bound variable by a free
   variable.  The free variable has type~$T$ and its name is a variant
-  of~$a$ choosen to be distinct from all constants and from all variables
+  of~$a$ chosen to be distinct from all constants and from all variables
   free in~$u$.
 
 \item[$t$ \ttindexbold{aconv} $u$] 

--- a/doc-src/Ref/thm.tex	Fri Apr 22 18:08:57 1994 +0200
+++ b/doc-src/Ref/thm.tex	Fri Apr 22 18:18:37 1994 +0200
@@ -92,7 +92,7 @@
 conclusion of $thm@1$ with the first premise of~$thm@2$.
 
 \item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS} 
-  uses {\tt RLN} to resolve $thm@i$ against premise~$i$ of $thm$, for
+  uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for
   $i=n$, \ldots,~1.  This applies $thm@n$, \ldots, $thm@1$ to the first $n$
   premises of $thm$.  Because the theorems are used from right to left, it
   does not matter if the $thm@i$ create new premises.  {\tt MRS} is useful
@@ -169,15 +169,15 @@
 \subsection{Miscellaneous forward rules}
 \index{theorems!standardizing}
 \begin{ttbox} 
-standard         : thm -> thm
-zero_var_indexes : thm -> thm
-make_elim        : thm -> thm
+standard         :           thm -> thm
+zero_var_indexes :           thm -> thm
+make_elim        :           thm -> thm
 rule_by_tactic   : tactic -> thm -> thm
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{standard} $thm$]  
 puts $thm$ into the standard form of object-rules.  It discharges all
-meta-hypotheses, replaces free variables by schematic variables, and
+meta-assumptions, replaces free variables by schematic variables, and
 renames schematic variables to have subscript zero.
 
 \item[\ttindexbold{zero_var_indexes} $thm$] 
@@ -228,7 +228,7 @@
 returns the flex-flex constraints of $thm$.
 
 \item[\ttindexbold{stamps_of_thm} $thm$] 
-returns the stamps of the signature associated with~$thm$.
+returns the \rmindex{stamps} of the signature associated with~$thm$.
 
 \item[\ttindexbold{dest_state} $(thm,i)$] 
 decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
@@ -237,7 +237,7 @@
 
 \item[\ttindexbold{rep_thm} $thm$] 
 decomposes $thm$ as a record containing the statement of~$thm$, its list of
-meta-hypotheses, the maximum subscript of its unknowns, and its signature.
+meta-assumptions, the maximum subscript of its unknowns, and its signature.
 \end{ttdescription}
 
 
@@ -284,12 +284,12 @@
 
 \index{meta-assumptions}
 The meta-logic uses natural deduction.  Each theorem may depend on
-meta-hypotheses, or assumptions.  Certain rules, such as $({\Imp}I)$,
+meta-level assumptions.  Certain rules, such as $({\Imp}I)$,
 discharge assumptions; in most other rules, the conclusion depends on all
 of the assumptions of the premises.  Formally, the system works with
 assertions of the form
 \[ \phi \quad [\phi@1,\ldots,\phi@n], \]
-where $\phi@1$,~\ldots,~$\phi@n$ are the hypotheses.  Do not confuse
+where $\phi@1$,~\ldots,~$\phi@n$ are the assumptions.  Do not confuse
 meta-level assumptions with the object-level assumptions in a subgoal,
 which are represented in the meta-logic using~$\Imp$.
 
@@ -299,7 +299,7 @@
 incompatible. 
 
 \index{meta-implication}
-The {\em implication\/} rules are $({\Imp}I)$
+The {\bf implication} rules are $({\Imp}I)$
 and $({\Imp}E)$:
 \[ \infer[({\Imp}I)]{\phi\Imp \psi}{\infer*{\psi}{[\phi]}}  \qquad
    \infer[({\Imp}E)]{\psi}{\phi\Imp \psi & \phi}  \]
@@ -311,7 +311,7 @@
    \qquad
    \infer[({\equiv}E)]{\psi}{\phi\equiv \psi & \phi}   \]
 
-The {\em equality\/} rules are reflexivity, symmetry, and transitivity:
+The {\bf equality} rules are reflexivity, symmetry, and transitivity:
 \[ {a\equiv a}\,(refl)  \qquad
    \infer[(sym)]{b\equiv a}{a\equiv b}  \qquad
    \infer[(trans)]{a\equiv c}{a\equiv b & b\equiv c}   \]
@@ -324,14 +324,14 @@
    {((\lambda x.a)(b)) \equiv a[b/x]}           \qquad
    \infer[(ext)]{f\equiv g}{f(x) \equiv g(x)}   \]
 
-The {\it abstraction\/} and {\it combination\/} rules permit the conversion
-of subterms:\footnote{Abstraction holds if $x$ is not free in the
+The {\bf abstraction} and {\bf combination} rules let conversions be
+applied to subterms:\footnote{Abstraction holds if $x$ is not free in the
 assumptions.}
 \[  \infer[(abs)]{(\lambda x.a) \equiv (\lambda x.b)}{a\equiv b}   \qquad
     \infer[(comb)]{f(a)\equiv g(b)}{f\equiv g & a\equiv b}   \]
 
 \index{meta-quantifiers}
-The {\em universal quantification\/} rules are $(\Forall I)$ and $(\Forall
+The {\bf universal quantification} rules are $(\Forall I)$ and $(\Forall
 E)$:\footnote{$(\Forall I)$ holds if $x$ is not free in the assumptions.}
 \[ \infer[(\Forall I)]{\Forall x.\phi}{\phi}        \qquad
    \infer[(\Forall E)]{\phi[b/x]}{\Forall x.\phi}   \]
@@ -344,9 +344,9 @@
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{assume} $ct$] 
-makes the theorem \(\phi \quad[\phi]\), where $\phi$ is the value of~$ct$.
+makes the theorem \(\phi \;[\phi]\), where $\phi$ is the value of~$ct$.
 The rule checks that $ct$ has type $prop$ and contains no unknowns, which
-are not allowed in hypotheses.
+are not allowed in assumptions.
 \end{ttdescription}
 
 \subsection{Implication rules}
@@ -361,15 +361,16 @@
 \begin{ttdescription}
 \item[\ttindexbold{implies_intr} $ct$ $thm$] 
 is $({\Imp}I)$, where $ct$ is the assumption to discharge, say~$\phi$.  It
-maps the premise $\psi\quad[\phi]$ to the conclusion $\phi\Imp\psi$.  The
-rule checks that $ct$ has type $prop$.
+maps the premise~$\psi$ to the conclusion $\phi\Imp\psi$, removing all
+occurrences of~$\phi$ from the assumptions.  The rule checks that $ct$ has
+type $prop$. 
 
 \item[\ttindexbold{implies_intr_list} $cts$ $thm$] 
 applies $({\Imp}I)$ repeatedly, on every element of the list~$cts$.
 
 \item[\ttindexbold{implies_intr_hyps} $thm$] 
-applies $({\Imp}I)$ to discharge all the hypotheses of~$thm$.  It maps the
-premise $\phi \quad [\phi@1,\ldots,\phi@n]$ to the conclusion
+applies $({\Imp}I)$ to discharge all the hypotheses (assumptions) of~$thm$.
+It maps the premise $\phi \; [\phi@1,\ldots,\phi@n]$ to the conclusion
 $\List{\phi@1,\ldots,\phi@n}\Imp\phi$.
 
 \item[\ttindexbold{implies_elim} $thm@1$ $thm@2$] 
@@ -390,8 +391,10 @@
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{equal_intr} $thm@1$ $thm@2$] 
-applies $({\equiv}I)$ to $thm@1$ and~$thm@2$.  It maps the premises
-$\psi\quad[\phi]$ and $\phi\quad[\psi]$ to the conclusion~$\phi\equiv\psi$.
+applies $({\equiv}I)$ to $thm@1$ and~$thm@2$.  It maps the premises~$\psi$
+and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
+the first premise with~$\phi$ removed, plus those of
+the second premise with~$\psi$ removed.
 
 \item[\ttindexbold{equal_elim} $thm@1$ $thm@2$] 
 applies $({\equiv}E)$ to $thm@1$ and~$thm@2$.  It maps the premises
@@ -436,14 +439,14 @@
 \item[\ttindexbold{extensional} $thm$] 
 maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
 Parameter~$x$ is taken from the premise.  It may be an unknown or a free
-variable (provided it does not occur in the hypotheses); it must not occur
+variable (provided it does not occur in the assumptions); it must not occur
 in $f$ or~$g$.
 
 \item[\ttindexbold{abstract_rule} $v$ $x$ $thm$] 
 maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
 (\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
 Parameter~$x$ is supplied as a cterm.  It may be an unknown or a free
-variable (provided it does not occur in the hypotheses).  In the
+variable (provided it does not occur in the assumptions).  In the
 conclusion, the bound variable is named~$v$.
 
 \item[\ttindexbold{combination} $thm@1$ $thm@2$] 
@@ -465,7 +468,7 @@
 applies $({\Forall}I)$, abstracting over all occurrences (if any!) of~$x$.
 The rule maps the premise $\phi$ to the conclusion $\Forall x.\phi$.
 Parameter~$x$ is supplied as a cterm.  It may be an unknown or a free
-variable (provided it does not occur in the hypotheses).
+variable (provided it does not occur in the assumptions).
 
 \item[\ttindexbold{forall_intr_list} $xs$ $thm$] 
 applies $({\Forall}I)$ repeatedly, on every element of the list~$xs$.
@@ -592,7 +595,7 @@
 analogous to {\tt RS}\@.  
 
 For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
-that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P)$, which is the
+that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
 principle of contrapositives.  Then the result would be the
 derived rule $\neg(b=a)\Imp\neg(a=b)$.