diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Advanced/document/simp.tex
--- a/doc-src/TutorialI/Advanced/document/simp.tex	Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex	Fri Jan 12 16:07:20 2001 +0100
@@ -13,10 +13,10 @@
 situation.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Advanced features%
+\isamarkupsubsection{Advanced Features%
 }
 %
-\isamarkupsubsubsection{Congruence rules%
+\isamarkupsubsubsection{Congruence Rules%
 }
 %
 \begin{isamarkuptext}%
@@ -58,7 +58,7 @@
 congruence rule for \isa{if}. Analogous rules control the evaluaton of
 \isa{case} expressions.
 
-You can delare your own congruence rules with the attribute \isa{cong},
+You can declare your own congruence rules with the attribute \isa{cong},
 either globally, in the usual manner,
 \begin{quote}
 \isacommand{declare} \textit{theorem-name} \isa{{\isacharbrackleft}cong{\isacharbrackright}}
@@ -74,11 +74,12 @@
 \begin{isabelle}%
 \ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}%
 \end{isabelle}
-is occasionally useful but not a default rule; you have to use it explicitly.
+\par\noindent
+is occasionally useful but is not a default rule; you have to declare it explicitly.
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Permutative rewrite rules%
+\isamarkupsubsubsection{Permutative Rewrite Rules%
 }
 %
 \begin{isamarkuptext}%
@@ -120,11 +121,11 @@
  f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
 
 Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely
-necessary because the builtin arithmetic capabilities often take care of
-this.%
+necessary because the built-in arithmetic prover often succeeds without
+such hints.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{How it works%
+\isamarkupsubsection{How It Works%
 }
 %
 \begin{isamarkuptext}%
@@ -134,7 +135,7 @@
 proved (again by simplification). Below we explain some special features of the rewriting process.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Higher-order patterns%
+\isamarkupsubsubsection{Higher-Order Patterns%
 }
 %
 \begin{isamarkuptext}%
@@ -158,7 +159,7 @@
 
 If the left-hand side is not a higher-order pattern, not all is lost
 and the simplifier will still try to apply the rule, but only if it
-matches ``directly'', i.e.\ without much $\lambda$-calculus hocus
+matches \emph{directly}, i.e.\ without much $\lambda$-calculus hocus
 pocus. For example, \isa{{\isacharquery}f\ {\isacharquery}x\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ True} rewrites
 \isa{g\ a\ {\isasymin}\ range\ g} to \isa{True}, but will fail to match
 \isa{g{\isacharparenleft}h\ b{\isacharparenright}\ {\isasymin}\ range{\isacharparenleft}{\isasymlambda}x{\isachardot}\ g{\isacharparenleft}h\ x{\isacharparenright}{\isacharparenright}}.  However, you can
@@ -166,25 +167,25 @@
 is not a pattern) by adding new variables and conditions: \isa{{\isacharquery}y\ {\isacharequal}\ {\isacharquery}f\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}y\ {\isasymin}\ range\ {\isacharquery}f\ {\isacharequal}\ True} is fine
 as a conditional rewrite rule since conditions can be arbitrary
 terms. However, this trick is not a panacea because the newly
-introduced conditions may be hard to prove, which has to take place
+introduced conditions may be hard to prove, as they must be
 before the rule can actually be applied.
   
-There is basically no restriction on the form of the right-hand
+There is no restriction on the form of the right-hand
 sides.  They may not contain extraneous term or type variables, though.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{The preprocessor%
+\isamarkupsubsubsection{The Preprocessor%
 }
 %
 \begin{isamarkuptext}%
 \label{sec:simp-preprocessor}
-When some theorem is declared a simplification rule, it need not be a
+When a theorem is declared a simplification rule, it need not be a
 conditional equation already.  The simplifier will turn it into a set of
-conditional equations automatically.  For example, given \isa{f\ x\ {\isacharequal}\ g\ x\ {\isasymand}\ h\ x\ {\isacharequal}\ k\ x} the simplifier will turn this into the two separate
-simplifiction rules \isa{f\ x\ {\isacharequal}\ g\ x} and \isa{h\ x\ {\isacharequal}\ k\ x}. In
+conditional equations automatically.  For example, \isa{f\ x\ {\isacharequal}\ g\ x\ {\isasymand}\ h\ x\ {\isacharequal}\ k\ x} becomes the two separate
+simplification rules \isa{f\ x\ {\isacharequal}\ g\ x} and \isa{h\ x\ {\isacharequal}\ k\ x}. In
 general, the input theorem is converted as follows:
 \begin{eqnarray}
-\neg P &\mapsto& P = False \nonumber\\
+\neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\
 P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
 P \land Q &\mapsto& P,\ Q \nonumber\\
 \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
@@ -193,11 +194,12 @@
  P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
 \end{eqnarray}
 Once this conversion process is finished, all remaining non-equations
-$P$ are turned into trivial equations $P = True$.
-For example, the formula \begin{center}\isa{{\isacharparenleft}p\ {\isasymlongrightarrow}\ q\ {\isasymand}\ r{\isacharparenright}\ {\isasymand}\ s}\end{center}
+$P$ are turned into trivial equations $P =\isa{True}$.
+For example, the formula 
+\begin{center}\isa{{\isacharparenleft}p\ {\isasymlongrightarrow}\ t\ {\isacharequal}\ u\ {\isasymand}\ {\isasymnot}\ r{\isacharparenright}\ {\isasymand}\ s}\end{center}
 is converted into the three rules
 \begin{center}
-\isa{p\ {\isasymLongrightarrow}\ q\ {\isacharequal}\ True},\quad  \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ True},\quad  \isa{s\ {\isacharequal}\ True}.
+\isa{p\ {\isasymLongrightarrow}\ t\ {\isacharequal}\ u},\quad  \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ False},\quad  \isa{s\ {\isacharequal}\ True}.
 \end{center}
 \index{simplification rule|)}
 \index{simplification|)}%