stylistic improvements

--- a/doc-src/Logics/CTT.tex	Wed May 07 17:16:18 1997 +0200
+++ b/doc-src/Logics/CTT.tex	Wed May 07 17:16:36 1997 +0200
@@ -669,7 +669,6 @@
 \tdx{div_def}           a div b ==
                   rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y.v))
 
-
 \tdx{add_typing}        [| a:N;  b:N |] ==> a #+ b : N
 \tdx{addC0}             b:N ==> 0 #+ b = b : N
 \tdx{addC_succ}         [| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N

--- a/doc-src/Logics/FOL.tex	Wed May 07 17:16:18 1997 +0200
+++ b/doc-src/Logics/FOL.tex	Wed May 07 17:16:36 1997 +0200
@@ -196,11 +196,6 @@
 \FOL{} instantiates most of Isabelle's generic packages.
 \begin{itemize}
 \item 
-Because it includes a general substitution rule, \FOL{} instantiates the
-tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
-throughout a subgoal and its hypotheses.
-(See {\tt FOL/ROOT.ML} for details.)
-\item 
 It instantiates the simplifier.  Both equality ($=$) and the biconditional
 ($\bimp$) may be used for rewriting.  Tactics such as {\tt Asm_simp_tac} and
 {\tt Full_simp_tac} use the default simpset ({\tt!simpset}), which works for
@@ -215,8 +210,19 @@
 \item 
 It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
 for details. 
+
+\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
+  for an equality throughout a subgoal and its hypotheses.  This tactic uses
+  \FOL's general substitution rule.
 \end{itemize}
 
+\begin{warn}\index{simplification!of conjunctions}%
+  Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The
+  left part of a conjunction helps in simplifying the right part.  This effect
+  is not available by default: it can be slow.  It can be obtained by
+  including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
+\end{warn}
+
 
 \section{Intuitionistic proof procedures} \label{fol-int-prover}
 Implication elimination (the rules~{\tt mp} and~{\tt impE}) pose
@@ -331,7 +337,7 @@
 well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
 rule (see Fig.\ts\ref{fol-cla-derived}).
 
-The classical reasoner is installed.  Tactics such as {\tt Fast_tac} and {\tt
+The classical reasoner is installed.  Tactics such as {\tt Blast_tac} and {\tt
 Best_tac} use the default claset ({\tt!claset}), which works for most
 purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
 propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
@@ -649,7 +655,7 @@
 \end{ttbox}
 The derivations of the introduction and elimination rules demonstrate the
 methods for rewriting with definitions.  Classical reasoning is required,
-so we use {\tt fast_tac}.
+so we use {\tt blast_tac}.
 
 
 \subsection{Deriving the introduction rule}
@@ -665,10 +671,10 @@
 {\out  1. P & Q | ~ P & R}
 \end{ttbox}
 The premises (bound to the {\ML} variable {\tt prems}) are passed as
-introduction rules to \ttindex{fast_tac}.  Remember that {\tt!claset} refers
+introduction rules to \ttindex{blast_tac}.  Remember that {\tt!claset} refers
 to the default classical set.
 \begin{ttbox}
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 {\out Level 1}
 {\out if(P,Q,R)}
 {\out No subgoals!}
@@ -689,14 +695,14 @@
 The major premise contains an occurrence of~$if$, but the version returned
 by \ttindex{goalw} (and bound to the {\ML} variable~{\tt major}) has the
 definition expanded.  Now \ttindex{cut_facts_tac} inserts~{\tt major} as an
-assumption in the subgoal, so that \ttindex{fast_tac} can break it down.
+assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
 \begin{ttbox}
 by (cut_facts_tac [major] 1);
 {\out Level 1}
 {\out S}
 {\out  1. P & Q | ~ P & R ==> S}
 \ttbreak
-by (fast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
 {\out Level 2}
 {\out S}
 {\out No subgoals!}
@@ -789,13 +795,13 @@
 AddSEs [ifE];
 \end{ttbox}
 Now we can revert to the
-initial proof state and let \ttindex{fast_tac} solve it.  
+initial proof state and let \ttindex{blast_tac} solve it.  
 \begin{ttbox}
 choplev 0;
 {\out Level 0}
 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
 {\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
-by (Fast_tac 1);
+by (Blast_tac 1);
 {\out Level 1}
 {\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
 {\out No subgoals!}
@@ -807,7 +813,7 @@
 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
 {\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
 \ttbreak
-by (Fast_tac 1);
+by (Blast_tac 1);
 {\out Level 1}
 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
 {\out No subgoals!}
@@ -816,7 +822,7 @@
 
 \subsection{Derived rules versus definitions}
 Dispensing with the derived rules, we can treat $if$ as an
-abbreviation, and let \ttindex{fast_tac} prove the expanded formula.  Let
+abbreviation, and let \ttindex{blast_tac} prove the expanded formula.  Let
 us redo the previous proof:
 \begin{ttbox}
 choplev 0;
@@ -834,9 +840,9 @@
 \end{ttbox}
 We are left with a subgoal in pure first-order logic, which is why the 
 classical reasoner can prove it given {\tt FOL_cs} alone.  (We could, of 
-course, have used {\tt Fast_tac}.)
+course, have used {\tt Blast_tac}.)
 \begin{ttbox}
-by (fast_tac FOL_cs 1);
+by (blast_tac FOL_cs 1);
 {\out Level 2}
 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
 {\out No subgoals!}
@@ -858,7 +864,7 @@
 {\out Level 0}
 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
 {\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
-by (Fast_tac 1);
+by (Blast_tac 1);
 {\out by: tactic failed}
 \end{ttbox}
 This failure message is uninformative, but we can get a closer look at the
@@ -889,7 +895,7 @@
 {\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
 {\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
 {\out     P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}
-by (fast_tac FOL_cs 1);
+by (blast_tac FOL_cs 1);
 {\out by: tactic failed}
 \end{ttbox}
 Again we apply \ttindex{step_tac}:

--- a/doc-src/Logics/ZF.tex	Wed May 07 17:16:18 1997 +0200
+++ b/doc-src/Logics/ZF.tex	Wed May 07 17:16:36 1997 +0200
@@ -65,7 +65,7 @@
 $x$ is a set.
 
 
-\begin{figure} 
+\begin{figure} \small
 \begin{center}
 \begin{tabular}{rrr} 
   \it name      &\it meta-type  & \it description \\ 
@@ -1243,7 +1243,7 @@
 have been proved.  These results are fundamental to a treatment of
 equipollence and cardinality.
 
-\begin{figure}
+\begin{figure}\small
 \index{#*@{\tt\#*} symbol}
 \index{*div symbol}
 \index{*mod symbol}
@@ -1293,9 +1293,8 @@
 \tdx{mult_type}     [| m:nat;  n:nat |] ==> m #* n : nat
 \tdx{mult_0}        0 #* n = 0
 \tdx{mult_succ}     succ(m) #* n = n #+ (m #* n)
-\tdx{mult_commute}  [| m:nat;  n:nat |] ==> m #* n = n #* m
-\tdx{add_mult_dist}
-    [| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)
+\tdx{mult_commute}  [| m:nat; n:nat |] ==> m #* n = n #* m
+\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)
 \tdx{mult_assoc}
     [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)
 \tdx{mod_quo_equality}
@@ -1689,24 +1688,23 @@
 \end{ttbox}
 \medskip
 We could have performed this proof in one step by applying
-\ttindex{Fast_tac}.  Let us
+\ttindex{Blast_tac}.  Let us
 go back to the start:
 \begin{ttbox}
 choplev 0;
 {\out Level 0}
 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
 {\out  1. Pow(A Int B) = Pow(A) Int Pow(B)}
-\end{ttbox}
-We must add \tdx{equalityI} as an introduction rule.
-Extensionality is not used by default: many equalities can be proved
-by rewriting.
-\begin{ttbox}
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Blast_tac 1);
+{\out Depth = 0}
+{\out Depth = 1}
+{\out Depth = 2}
+{\out Depth = 3}
 {\out Level 1}
 {\out Pow(A Int B) = Pow(A) Int Pow(B)}
 {\out No subgoals!}
 \end{ttbox}
-In the past this was regarded as a difficult proof, as indeed it is if all
+Past researchers regarded this as a difficult proof, as indeed it is if all
 the symbols are replaced by their definitions.
 \goodbreak
 
@@ -1765,14 +1763,31 @@
 {\out Union(C) <= Union(D)}
 {\out No subgoals!}
 \end{ttbox}
-Again, \ttindex{fast_tac} can prove the theorem in one
-step, provided we somehow supply it with~{\tt prem}.  We can either add
-this premise to the assumptions using \ttindex{cut_facts_tac}, or add
-\hbox{\tt prem RS subsetD} to the claset as an introduction rule.
+Again, \ttindex{Blast_tac} can prove the theorem in one
+step, provided we somehow supply it with~{\tt prem}.  We can add
+\hbox{\tt prem RS subsetD} to the claset as an introduction rule:
+\begin{ttbox}
+by (blast_tac (!claset addIs [prem RS subsetD]) 1);
+{\out Depth = 0}
+{\out Depth = 1}
+{\out Depth = 2}
+{\out Level 1}
+{\out Union(C) <= Union(D)}
+{\out No subgoals!}
+\end{ttbox}
+As an alternative, we could add premise to the assumptions, either using
+\ttindex{cut_facts_tac} or by stating the original goal using~\texttt{!!}:
+\begin{ttbox}
+goal thy "!!C D. C<=D ==> Union(C) <= Union(D)";
+{\out Level 0}
+{\out Union(C) <= Union(D)}
+{\out  1. !!C D. C <= D ==> Union(C) <= Union(D)}
+by (Blast_tac 1);
+\end{ttbox}
 
 The file {\tt ZF/equalities.ML} has many similar proofs.  Reasoning about
 general intersection can be difficult because of its anomalous behaviour on
-the empty set.  However, \ttindex{fast_tac} copes well with these.  Here is
+the empty set.  However, \ttindex{Blast_tac} copes well with these.  Here is
 a typical example, borrowed from Devlin~\cite[page 12]{devlin79}:
 \begin{ttbox}
 a:C ==> (INT x:C. A(x) Int B(x)) = (INT x:C.A(x)) Int (INT x:C.B(x))