minor edits to Chapters 1-3

--- a/doc-src/TutorialI/Advanced/WFrec.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -79,7 +79,7 @@
 by simp;
 
 text{*\noindent
-and should have appended the following hint to our above definition:
+and should have appended the following hint to our definition above:
 \indexbold{*recdef_wf}
 *}
 (*<*)

--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -76,7 +76,7 @@
 \isacommand{by}\ simp%
 \begin{isamarkuptext}%
 \noindent
-and should have appended the following hint to our above definition:
+and should have appended the following hint to our definition above:
 \indexbold{*recdef_wf}%
 \end{isamarkuptext}%
 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}%

--- a/doc-src/TutorialI/Advanced/document/simp.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -93,7 +93,7 @@
 once they apply, they can be used forever. The simplifier is aware of this
 danger and treats permutative rules by means of a special strategy, called
 \bfindex{ordered rewriting}: a permutative rewrite
-rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed
+rule is only applied if the term becomes ``smaller'' (with respect to a fixed
 lexicographic ordering on terms). For example, commutativity rewrites
 \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly
 smaller than \isa{b\ {\isacharplus}\ a}.  Permutative rewrite rules can be turned into

--- a/doc-src/TutorialI/Advanced/simp.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Advanced/simp.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -78,7 +78,7 @@
 once they apply, they can be used forever. The simplifier is aware of this
 danger and treats permutative rules by means of a special strategy, called
 \bfindex{ordered rewriting}: a permutative rewrite
-rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed
+rule is only applied if the term becomes ``smaller'' (with respect to a fixed
 lexicographic ordering on terms). For example, commutativity rewrites
 @{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
 smaller than @{term"b+a"}.  Permutative rewrite rules can be turned into

--- a/doc-src/TutorialI/CTL/Base.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -4,9 +4,9 @@
 
 text{*\label{sec:VMC}
 Model checking is a very popular technique for the verification of finite
-state systems (implementations) w.r.t.\ temporal logic formulae
+state systems (implementations) with respect to temporal logic formulae
 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
-and this section shall explore them a little in HOL. This is done in two steps: first
+and this section will explore them a little in HOL\@. This is done in two steps: first
 we consider a simple modal logic called propositional dynamic
 logic (PDL) which we then extend to the temporal logic CTL used in many real
 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a

--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -346,7 +346,7 @@
 
 text{*
 
-The above language is not quite CTL. The latter also includes an
+The above language is not quite CTL\@. The latter also includes an
 until-operator @{term"EU f g"} with semantics ``there exist a path
 where @{term f} is true until @{term g} becomes true''. With the help
 of an auxiliary function

--- a/doc-src/TutorialI/CTL/CTLind.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -7,7 +7,7 @@
 some of the induction principles and heuristics discussed above and we want to
 show how inductive definitions can simplify proofs.
 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
-model checker for CTL. In particular the proof of the
+model checker for CTL\@. In particular the proof of the
 @{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
 simple as one might intuitively expect, due to the @{text SOME} operator
 involved. Below we give a simpler proof of @{thm[source]AF_lemma2}

--- a/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -8,9 +8,9 @@
 \begin{isamarkuptext}%
 \label{sec:VMC}
 Model checking is a very popular technique for the verification of finite
-state systems (implementations) w.r.t.\ temporal logic formulae
+state systems (implementations) with respect to temporal logic formulae
 (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
-and this section shall explore them a little in HOL. This is done in two steps: first
+and this section will explore them a little in HOL\@. This is done in two steps: first
 we consider a simple modal logic called propositional dynamic
 logic (PDL) which we then extend to the temporal logic CTL used in many real
 model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -281,7 +281,7 @@
 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline
 \isacommand{done}%
 \begin{isamarkuptext}%
-The above language is not quite CTL. The latter also includes an
+The above language is not quite CTL\@. The latter also includes an
 until-operator \isa{EU\ f\ g} with semantics ``there exist a path
 where \isa{f} is true until \isa{g} becomes true''. With the help
 of an auxiliary function%

--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -11,7 +11,7 @@
 some of the induction principles and heuristics discussed above and we want to
 show how inductive definitions can simplify proofs.
 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
-model checker for CTL. In particular the proof of the
+model checker for CTL\@. In particular the proof of the
 \isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as
 simple as one might intuitively expect, due to the \isa{SOME} operator
 involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}}

--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -6,7 +6,7 @@
 
 text{*\label{sec:ExprCompiler}
 The task is to develop a compiler from a generic type of expressions (built
-up from variables, constants and binary operations) to a stack machine.  This
+from variables, constants and binary operations) to a stack machine.  This
 generic type of expressions is a generalization of the boolean expressions in
 \S\ref{sec:boolex}.  This time we do not commit ourselves to a particular
 type of variables or values but make them type parameters.  Neither is there
@@ -23,7 +23,7 @@
 The three constructors represent constants, variables and the application of
 a binary operation to two subexpressions.
 
-The value of an expression w.r.t.\ an environment that maps variables to
+The value of an expression with respect to an environment that maps variables to
 values is easily defined:
 *}
 
@@ -35,7 +35,7 @@
 
 text{*
 The stack machine has three instructions: load a constant value onto the
-stack, load the contents of a certain address onto the stack, and apply a
+stack, load the contents of an address onto the stack, and apply a
 binary operation to the two topmost elements of the stack, replacing them by
 the result. As for @{text"expr"}, addresses and values are type parameters:
 *}
@@ -66,12 +66,12 @@
 return the first element and the remainder of a list.
 Because all functions are total, @{term"hd"} is defined even for the empty
 list, although we do not know what the result is. Thus our model of the
-machine always terminates properly, although the above definition does not
+machine always terminates properly, although the definition above does not
 tell us much about the result in situations where @{term"Apply"} was executed
 with fewer than two elements on the stack.
 
 The compiler is a function from expressions to a list of instructions. Its
-definition is pretty much obvious:
+definition is obvious:
 *}
 
 consts comp :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list";

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -8,7 +8,7 @@
 \begin{isamarkuptext}%
 \label{sec:ExprCompiler}
 The task is to develop a compiler from a generic type of expressions (built
-up from variables, constants and binary operations) to a stack machine.  This
+from variables, constants and binary operations) to a stack machine.  This
 generic type of expressions is a generalization of the boolean expressions in
 \S\ref{sec:boolex}.  This time we do not commit ourselves to a particular
 type of variables or values but make them type parameters.  Neither is there
@@ -24,7 +24,7 @@
 The three constructors represent constants, variables and the application of
 a binary operation to two subexpressions.
 
-The value of an expression w.r.t.\ an environment that maps variables to
+The value of an expression with respect to an environment that maps variables to
 values is easily defined:%
 \end{isamarkuptext}%
 \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline
@@ -34,7 +34,7 @@
 {\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e{\isadigit{1}}\ env{\isacharparenright}\ {\isacharparenleft}value\ e{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 The stack machine has three instructions: load a constant value onto the
-stack, load the contents of a certain address onto the stack, and apply a
+stack, load the contents of an address onto the stack, and apply a
 binary operation to the two topmost elements of the stack, replacing them by
 the result. As for \isa{expr}, addresses and values are type parameters:%
 \end{isamarkuptext}%
@@ -62,12 +62,12 @@
 return the first element and the remainder of a list.
 Because all functions are total, \isa{hd} is defined even for the empty
 list, although we do not know what the result is. Thus our model of the
-machine always terminates properly, although the above definition does not
+machine always terminates properly, although the definition above does not
 tell us much about the result in situations where \isa{Apply} was executed
 with fewer than two elements on the stack.
 
 The compiler is a function from expressions to a list of instructions. Its
-definition is pretty much obvious:%
+definition is obvious:%
 \end{isamarkuptext}%
 \isacommand{consts}\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequote}\isanewline
 \isacommand{primrec}\isanewline

--- a/doc-src/TutorialI/Datatype/Fundata.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -32,7 +32,7 @@
 Isabelle because the termination proof is not as obvious since
 @{term"map_bt"} is only partially applied.
 
-The following lemma has a canonical proof  *}
+The following lemma has a canonical proof:  *}
 
 lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
 apply(induct_tac T, simp_all)
@@ -40,8 +40,9 @@
 (*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
 apply(induct_tac T, rename_tac[2] F)(*>*)
 txt{*\noindent
-but it is worth taking a look at the proof state after the induction step
-to understand what the presence of the function type entails:
+It is worth taking a look at the proof state after the induction step
+to understand what the presence of the function type entails.
+Notice the quantified induction hypothesis:
 @{subgoals[display,indent=0]}
 *}
 (*<*)

--- a/doc-src/TutorialI/Datatype/Nested.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -89,13 +89,13 @@
   term. Prove that @{prop"trev(trev t) = t"}.
 \end{exercise}
 
-The experienced functional programmer may feel that our above definition of
-@{term subst} is unnecessarily complicated in that @{term substs} is
-completely unnecessary. The @{term App}-case can be defined directly as
+The experienced functional programmer may feel that our definition of
+@{term subst} is too complicated in that @{term substs} is
+unnecessary. The @{term App}-case can be defined directly as
 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
 where @{term"map"} is the standard list function such that
 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
-insists on the above fixed format. Fortunately, we can easily \emph{prove}
+insists on the conjunctive format. Fortunately, we can easily \emph{prove}
 that the suggested equation holds:
 *}
 
@@ -116,8 +116,8 @@
 about @{term map}.  Unfortunately inductive proofs about type
 @{text term} are still awkward because they expect a conjunction. One
 could derive a new induction principle as well (see
-\S\ref{sec:derive-ind}), but turns out to be simpler to define
-functions by \isacommand{recdef} instead of \isacommand{primrec}.
+\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
+and to define functions with \isacommand{recdef} instead.
 The details are explained in \S\ref{sec:nested-recdef} below.
 
 Of course, you may also combine mutual and nested recursion. For example,

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -33,15 +33,16 @@
 Isabelle because the termination proof is not as obvious since
 \isa{map{\isacharunderscore}bt} is only partially applied.
 
-The following lemma has a canonical proof%
+The following lemma has a canonical proof:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
 \isacommand{done}%
 \begin{isamarkuptxt}%
 \noindent
-but it is worth taking a look at the proof state after the induction step
-to understand what the presence of the function type entails:
+It is worth taking a look at the proof state after the induction step
+to understand what the presence of the function type entails.
+Notice the quantified induction hypothesis:
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline
 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline

--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -87,15 +87,15 @@
   term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}.
 \end{exercise}
 
-The experienced functional programmer may feel that our above definition of
-\isa{subst} is unnecessarily complicated in that \isa{substs} is
-completely unnecessary. The \isa{App}-case can be defined directly as
+The experienced functional programmer may feel that our definition of
+\isa{subst} is too complicated in that \isa{substs} is
+unnecessary. The \isa{App}-case can be defined directly as
 \begin{isabelle}%
 \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
 \end{isabelle}
 where \isa{map} is the standard list function such that
 \isa{map\ f\ {\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle
-insists on the above fixed format. Fortunately, we can easily \emph{prove}
+insists on the conjunctive format. Fortunately, we can easily \emph{prove}
 that the suggested equation holds:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline
@@ -114,8 +114,8 @@
 about \isa{map}.  Unfortunately inductive proofs about type
 \isa{term} are still awkward because they expect a conjunction. One
 could derive a new induction principle as well (see
-\S\ref{sec:derive-ind}), but turns out to be simpler to define
-functions by \isacommand{recdef} instead of \isacommand{primrec}.
+\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
+and to define functions with \isacommand{recdef} instead.
 The details are explained in \S\ref{sec:nested-recdef} below.
 
 Of course, you may also combine mutual and nested recursion. For example,

--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -36,12 +36,12 @@
 values:
 *}
 
-consts value :: "boolex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
+consts value :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
 primrec
 "value (Const b) env = b"
 "value (Var x)   env = env x"
-"value (Neg b)   env = (\\<not> value b env)"
-"value (And b c) env = (value b env \\<and> value c env)";
+"value (Neg b)   env = (\<not> value b env)"
+"value (And b c) env = (value b env \<and> value c env)";
 
 text{*\noindent
 \subsubsection{If-expressions}
@@ -58,7 +58,7 @@
 The evaluation if If-expressions proceeds as for @{typ"boolex"}:
 *}
 
-consts valif :: "ifex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
+consts valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool";
 primrec
 "valif (CIF b)    env = b"
 "valif (VIF x)    env = env x"
@@ -73,7 +73,7 @@
 translate from @{typ"boolex"} into @{typ"ifex"}:
 *}
 
-consts bool2if :: "boolex \\<Rightarrow> ifex";
+consts bool2if :: "boolex \<Rightarrow> ifex";
 primrec
 "bool2if (Const b) = CIF b"
 "bool2if (Var x)   = VIF x"
@@ -107,13 +107,13 @@
 primitive recursive functions perform this task:
 *}
 
-consts normif :: "ifex \\<Rightarrow> ifex \\<Rightarrow> ifex \\<Rightarrow> ifex";
+consts normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex";
 primrec
 "normif (CIF b)    t e = IF (CIF b) t e"
 "normif (VIF x)    t e = IF (VIF x) t e"
 "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)";
 
-consts norm :: "ifex \\<Rightarrow> ifex";
+consts norm :: "ifex \<Rightarrow> ifex";
 primrec
 "norm (CIF b)    = CIF b"
 "norm (VIF x)    = VIF x"
@@ -133,7 +133,7 @@
 *}
 
 lemma [simp]:
-  "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
+  "\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
 (*<*)
 apply(induct_tac b);
 by(auto);
@@ -150,19 +150,19 @@
 the above sense? We define a function that tests If-expressions for normality
 *}
 
-consts normal :: "ifex \\<Rightarrow> bool";
+consts normal :: "ifex \<Rightarrow> bool";
 primrec
 "normal(CIF b) = True"
 "normal(VIF x) = True"
-"normal(IF b t e) = (normal t \\<and> normal e \\<and>
-     (case b of CIF b \\<Rightarrow> True | VIF x \\<Rightarrow> True | IF x y z \\<Rightarrow> False))";
+"normal(IF b t e) = (normal t \<and> normal e \<and>
+     (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))";
 
 text{*\noindent
 and prove @{term"normal(norm b)"}. Of course, this requires a lemma about
 normality of @{term"normif"}:
 *}
 
-lemma[simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
+lemma[simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)";
 (*<*)
 apply(induct_tac b);
 by(auto);
@@ -173,9 +173,9 @@
 (*>*)
 
 text{*\medskip
-How does one come up with the required lemmas? Try to prove the main theorems
-without them and study carefully what @{text auto} leaves unproved. This has
-to provide the clue.  The necessity of universal quantification
+How do we come up with the required lemmas? Try to prove the main theorems
+without them and study carefully what @{text auto} leaves unproved. This 
+can provide the clue.  The necessity of universal quantification
 (@{text"\<forall>t e"}) in the two lemmas is explained in
 \S\ref{sec:InductionHeuristics}
 

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -148,9 +148,9 @@
 \isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \medskip
-How does one come up with the required lemmas? Try to prove the main theorems
-without them and study carefully what \isa{auto} leaves unproved. This has
-to provide the clue.  The necessity of universal quantification
+How do we come up with the required lemmas? Try to prove the main theorems
+without them and study carefully what \isa{auto} leaves unproved. This 
+can provide the clue.  The necessity of universal quantification
 (\isa{{\isasymforall}t\ e}) in the two lemmas is explained in
 \S\ref{sec:InductionHeuristics}
 

--- a/doc-src/TutorialI/Misc/Itrev.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -64,7 +64,7 @@
 @{subgoals[display,indent=0,margin=65]}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed
-@{term"[]"}. The corresponding heuristic:
+argument, @{term"[]"}.  This suggests a heuristic:
 \begin{quote}
 \emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
@@ -109,11 +109,13 @@
 provability of the goal. Because it is not always required, and may even
 complicate matters in some cases, this heuristic is often not
 applied blindly.
+The variables that require generalization are typically those that 
+change in recursive calls.
 
 In general, if you have tried the above heuristics and still find your
 induction does not go through, and no obvious lemma suggests itself, you may
 need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb. In a nutshell: you
+the problem at hand and is beyond simple rules of thumb.  You
 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
 to learn about some advanced techniques for inductive proofs.
 

--- a/doc-src/TutorialI/Misc/Tree.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/Tree.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -8,14 +8,14 @@
 
 datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
 
-consts mirror :: "'a tree \\<Rightarrow> 'a tree";
+consts mirror :: "'a tree \<Rightarrow> 'a tree";
 primrec
 "mirror Tip = Tip"
 "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
 
 text{*\noindent
 and a function @{term"mirror"} that mirrors a binary tree
-by swapping subtrees (recursively). Prove
+by swapping subtrees recursively. Prove
 *}
 
 lemma mirror_mirror: "mirror(mirror t) = t";

--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -67,7 +67,7 @@
 \end{isabelle}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed
-\isa{{\isacharbrackleft}{\isacharbrackright}}. The corresponding heuristic:
+argument, \isa{{\isacharbrackleft}{\isacharbrackright}}.  This suggests a heuristic:
 \begin{quote}
 \emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
@@ -111,11 +111,13 @@
 provability of the goal. Because it is not always required, and may even
 complicate matters in some cases, this heuristic is often not
 applied blindly.
+The variables that require generalization are typically those that 
+change in recursive calls.
 
 In general, if you have tried the above heuristics and still find your
 induction does not go through, and no obvious lemma suggests itself, you may
 need to generalize your proposition even further. This requires insight into
-the problem at hand and is beyond simple rules of thumb. In a nutshell: you
+the problem at hand and is beyond simple rules of thumb.  You
 will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind}
 to learn about some advanced techniques for inductive proofs.
 

--- a/doc-src/TutorialI/Misc/document/Tree.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/Tree.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -10,7 +10,7 @@
 \begin{isamarkuptext}%
 \noindent
 and a function \isa{mirror} that mirrors a binary tree
-by swapping subtrees (recursively). Prove%
+by swapping subtrees recursively. Prove%
 \end{isamarkuptext}%
 \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}%
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/document/pairs.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/pairs.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -24,9 +24,10 @@
 Products, like type \isa{nat}, are datatypes, which means
 in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to
 terms of product type.
+Both replace the term by tuple of variables.
 \item
-Instead of tuples with many components (where ``many'' is not much above 2),
-it is preferable to use records.
+Tuples with more than two or three components become unwieldy;
+records are preferable.
 \end{itemize}
 For more information on pairs and records see Chapter~\ref{ch:more-types}.%
 \end{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -8,7 +8,7 @@
 \begin{isamarkuptext}%
 \indexbold{simplification rule}
 To facilitate simplification, theorems can be declared to be simplification
-rules (with the help of the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp
+rules (by the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp
   (attribute)}), in which case proofs by simplification make use of these
 rules automatically. In addition the constructs \isacommand{datatype} and
 \isacommand{primrec} (and a few others) invisibly declare useful
@@ -33,7 +33,7 @@
 proofs.  Frequent changes in the simplification status of a theorem may
 indicate a badly designed theory.
 \begin{warn}
-  Simplification may not terminate, for example if both $f(x) = g(x)$ and
+  Simplification may run forever, for example if both $f(x) = g(x)$ and
   $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
   to include simplification rules that can lead to nontermination, either on
   their own or in combination with other simplification rules.
@@ -49,7 +49,7 @@
 \begin{quote}
 \isa{simp} \textit{list of modifiers}
 \end{quote}
-where the list of \emph{modifiers} helps to fine tune the behaviour and may
+where the list of \emph{modifiers} fine tunes the behaviour and may
 be empty. Most if not all of the proofs seen so far could have been performed
 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
 only the first subgoal and may thus need to be repeated---use
@@ -120,10 +120,9 @@
  means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
-Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify
-the above problematic subgoal.
-
-Note that only one of the above options is allowed, and it must precede all
+Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on
+the problematic subgoal above.
+Note that only one of the options is allowed, and it must precede all
 other arguments.%
 \end{isamarkuptext}%
 %
@@ -183,7 +182,7 @@
 \index{simplification!of let-expressions}
 Proving a goal containing \isaindex{let}-expressions almost invariably
 requires the \isa{let}-con\-structs to be expanded at some point. Since
-\isa{let}-\isa{in} is just syntactic sugar for a predefined constant
+\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for a predefined constant
 (called \isa{Let}), expanding \isa{let}-constructs means rewriting with
 \isa{Let{\isacharunderscore}def}:%
 \end{isamarkuptext}%
@@ -211,13 +210,13 @@
 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
 sequence of methods. Assuming that the simplification rule
 \isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}}
-is present as well,%
+is present as well,
+the lemma below is proved by plain simplification:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-is proved by plain simplification:
-the conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above
+The conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above
 can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs}
 because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}
 simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local
@@ -327,8 +326,8 @@
 \index{arithmetic}
 The simplifier routinely solves a small class of linear arithmetic formulae
 (over type \isa{nat} and other numeric types): it only takes into account
-assumptions and conclusions that are (possibly negated) (in)equalities
-(\isa{{\isacharequal}}, \isasymle, \isa{{\isacharless}}) and it only knows about addition. Thus%
+assumptions and conclusions that are relations
+($=$, $\le$, $<$, possibly negated) and it only knows about addition. Thus%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}%
 \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Misc/pairs.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/pairs.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -22,9 +22,10 @@
 Products, like type @{typ nat}, are datatypes, which means
 in particular that @{text induct_tac} and @{text case_tac} are applicable to
 terms of product type.
+Both replace the term by tuple of variables.
 \item
-Instead of tuples with many components (where ``many'' is not much above 2),
-it is preferable to use records.
+Tuples with more than two or three components become unwieldy;
+records are preferable.
 \end{itemize}
 For more information on pairs and records see Chapter~\ref{ch:more-types}.
 *}

--- a/doc-src/TutorialI/Misc/simp.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -6,7 +6,7 @@
 
 text{*\indexbold{simplification rule}
 To facilitate simplification, theorems can be declared to be simplification
-rules (with the help of the attribute @{text"[simp]"}\index{*simp
+rules (by the attribute @{text"[simp]"}\index{*simp
   (attribute)}), in which case proofs by simplification make use of these
 rules automatically. In addition the constructs \isacommand{datatype} and
 \isacommand{primrec} (and a few others) invisibly declare useful
@@ -32,7 +32,7 @@
 proofs.  Frequent changes in the simplification status of a theorem may
 indicate a badly designed theory.
 \begin{warn}
-  Simplification may not terminate, for example if both $f(x) = g(x)$ and
+  Simplification may run forever, for example if both $f(x) = g(x)$ and
   $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
   to include simplification rules that can lead to nontermination, either on
   their own or in combination with other simplification rules.
@@ -46,7 +46,7 @@
 \begin{quote}
 @{text simp} \textit{list of modifiers}
 \end{quote}
-where the list of \emph{modifiers} helps to fine tune the behaviour and may
+where the list of \emph{modifiers} fine tunes the behaviour and may
 be empty. Most if not all of the proofs seen so far could have been performed
 with @{text simp} instead of \isa{auto}, except that @{text simp} attacks
 only the first subgoal and may thus need to be repeated---use
@@ -117,10 +117,9 @@
  means that the assumptions are simplified but are not
   used in the simplification of each other or the conclusion.
 \end{description}
-Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify
-the above problematic subgoal.
-
-Note that only one of the above options is allowed, and it must precede all
+Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on
+the problematic subgoal above.
+Note that only one of the options is allowed, and it must precede all
 other arguments.
 *}
 
@@ -177,7 +176,7 @@
 text{*\index{simplification!of let-expressions}
 Proving a goal containing \isaindex{let}-expressions almost invariably
 requires the @{text"let"}-con\-structs to be expanded at some point. Since
-@{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant
+@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for a predefined constant
 (called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
 @{thm[source]Let_def}:
 *}
@@ -209,6 +208,7 @@
 sequence of methods. Assuming that the simplification rule
 @{term"(rev xs = []) = (xs = [])"}
 is present as well,
+the lemma below is proved by plain simplification:
 *}
 
 lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
@@ -216,8 +216,7 @@
 by(simp);
 (*>*)
 text{*\noindent
-is proved by plain simplification:
-the conditional equation @{thm[source]hd_Cons_tl} above
+The conditional equation @{thm[source]hd_Cons_tl} above
 can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"}
 because the corresponding precondition @{term"rev xs ~= []"}
 simplifies to @{term"xs ~= []"}, which is exactly the local
@@ -333,8 +332,8 @@
 text{*\index{arithmetic}
 The simplifier routinely solves a small class of linear arithmetic formulae
 (over type \isa{nat} and other numeric types): it only takes into account
-assumptions and conclusions that are (possibly negated) (in)equalities
-(@{text"="}, \isasymle, @{text"<"}) and it only knows about addition. Thus
+assumptions and conclusions that are relations
+($=$, $\le$, $<$, possibly negated) and it only knows about addition. Thus
 *}
 
 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"

--- a/doc-src/TutorialI/Recdef/Induction.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -16,14 +16,15 @@
 requires you to prove for each \isacommand{recdef} equation that the property
 you are trying to establish holds for the left-hand side provided it holds
 for all recursive calls on the right-hand side. Here is a simple example
+involving the predefined @{term"map"} functional on lists:
 *}
 
 lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
 
 txt{*\noindent
-involving the predefined @{term"map"} functional on lists: @{term"map f xs"}
+Note that @{term"map f xs"}
 is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove
-this lemma by recursion induction w.r.t. @{term"sep"}:
+this lemma by recursion induction over @{term"sep"}:
 *}
 
 apply(induct_tac x xs rule: sep.induct);
@@ -46,7 +47,7 @@
 
 In general, the format of invoking recursion induction is
 \begin{quote}
-\isacommand{apply}@{text"(induct_tac ("}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
+\isacommand{apply}@{text"(induct_tac "}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
 \end{quote}\index{*induct_tac}%
 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
 name of a function that takes an $n$-tuple. Usually the subgoal will

--- a/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -15,14 +15,15 @@
 \textbf{recursion induction}. Roughly speaking, it
 requires you to prove for each \isacommand{recdef} equation that the property
 you are trying to establish holds for the left-hand side provided it holds
-for all recursive calls on the right-hand side. Here is a simple example%
+for all recursive calls on the right-hand side. Here is a simple example
+involving the predefined \isa{map} functional on lists:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
-involving the predefined \isa{map} functional on lists: \isa{map\ f\ xs}
+Note that \isa{map\ f\ xs}
 is the result of applying \isa{f} to all elements of \isa{xs}. We prove
-this lemma by recursion induction w.r.t. \isa{sep}:%
+this lemma by recursion induction over \isa{sep}:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
@@ -48,7 +49,7 @@
 
 In general, the format of invoking recursion induction is
 \begin{quote}
-\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ {\isacharparenleft}}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
+\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ }$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}}
 \end{quote}\index{*induct_tac}%
 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
 name of a function that takes an $n$-tuple. Usually the subgoal will

--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -75,7 +75,8 @@
 In fact, this is probably the neatest solution next to pattern matching.
 
 A final alternative is to replace the offending simplification rules by
-derived conditional ones. For \isa{gcd} it means we have to prove%
+derived conditional ones. For \isa{gcd} it means we have to prove
+these lemmas:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
@@ -85,7 +86,7 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
-after which we can disable the original simplification rule:%
+Now we can disable the original simplification rule:%
 \end{isamarkuptext}%
 \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline
 \end{isabellebody}%

--- a/doc-src/TutorialI/Recdef/document/termination.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -13,8 +13,8 @@
 the same function. What is more, those equations are automatically declared as
 simplification rules.
 
-In general, Isabelle may not be able to prove all termination conditions
-(there is one for each recursive call) automatically. For example,
+Isabelle may fail to prove some termination conditions
+(there is one for each recursive call).  For example,
 termination of the following artificial function%
 \end{isamarkuptext}%
 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
@@ -22,8 +22,8 @@
 \ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-is not proved automatically (although maybe it should be). Isabelle prints a
-kind of error message showing you what it was unable to prove. You will then
+is not proved automatically. Isabelle prints a
+message showing you what it was unable to prove. You will then
 have to prove it as a separate lemma before you attempt the definition
 of your function once more. In our case the required lemma is the obvious one:%
 \end{isamarkuptext}%

--- a/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -72,6 +72,7 @@
 
 A final alternative is to replace the offending simplification rules by
 derived conditional ones. For @{term gcd} it means we have to prove
+these lemmas:
 *}
 
 lemma [simp]: "gcd (m, 0) = m";
@@ -82,7 +83,7 @@
 done
 
 text{*\noindent
-after which we can disable the original simplification rule:
+Now we can disable the original simplification rule:
 *}
 
 declare gcd.simps [simp del]

--- a/doc-src/TutorialI/Recdef/termination.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -13,8 +13,8 @@
 the same function. What is more, those equations are automatically declared as
 simplification rules.
 
-In general, Isabelle may not be able to prove all termination conditions
-(there is one for each recursive call) automatically. For example,
+Isabelle may fail to prove some termination conditions
+(there is one for each recursive call).  For example,
 termination of the following artificial function
 *}
 
@@ -23,8 +23,8 @@
   "f(x,y) = (if x \<le> y then x else f(x,y+1))";
 
 text{*\noindent
-is not proved automatically (although maybe it should be). Isabelle prints a
-kind of error message showing you what it was unable to prove. You will then
+is not proved automatically. Isabelle prints a
+message showing you what it was unable to prove. You will then
 have to prove it as a separate lemma before you attempt the definition
 of your function once more. In our case the required lemma is the obvious one:
 *}

--- a/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -84,7 +84,7 @@
   done;
 
 theorem gcd_greatest_iff [iff]: 
-        "k dvd gcd(m,n) = (k dvd m \<and> k dvd n)"
+        "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)"
   apply (blast intro!: gcd_greatest intro: dvd_trans);
   done;
 

--- a/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -30,12 +30,11 @@
 and not as @{text"(x # y) # z"}.
 
 \begin{warn}
-  Syntax annotations are a powerful but completely optional feature. You
+  Syntax annotations are a powerful but optional feature. You
   could drop them from theory @{text"ToyList"} and go back to the identifiers
-  @{term[source]Nil} and @{term[source]Cons}. However, lists are such a
-  central datatype
-  that their syntax is highly customized. We recommend that novices should
-  not use syntax annotations in their own theories.
+  @{term[source]Nil} and @{term[source]Cons}.
+  We recommend that novices avoid using
+  syntax annotations in their own theories.
 \end{warn}
 Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
 *}
@@ -79,8 +78,8 @@
 % However, this is a subtle issue that we cannot discuss here further.
 
 \begin{warn}
-  As we have indicated, the desire for total functions is not a gratuitously
-  imposed restriction but an essential characteristic of HOL. It is only
+  As we have indicated, the requirement for total functions is not a gratuitous
+  restriction but an essential characteristic of HOL\@. It is only
   because of totality that reasoning in HOL is comparatively easy.  More
   generally, the philosophy in HOL is not to allow arbitrary axioms (such as
   function definitions whose totality has not been proved) because they
@@ -116,7 +115,7 @@
 illustrate not just the basic proof commands but also the typical proof
 process.
 
-\subsubsection*{Main goal: @{text"rev(rev xs) = xs"}}
+\subsubsection*{Main goal: @{text"rev(rev xs) = xs"}.}
 
 Our goal is to show that reversing a list twice produces the original
 list. The input line
@@ -125,6 +124,8 @@
 theorem rev_rev [simp]: "rev(rev xs) = xs";
 
 txt{*\index{*theorem|bold}\index{*simp (attribute)|bold}
+\noindent
+does several things.  It
 \begin{itemize}
 \item
 establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"},
@@ -231,7 +232,7 @@
 
 txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
 \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
-the importance we attach to a proposition. In general, we use the words
+the importance we attach to a proposition.  We use the words
 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
 interchangeably.
 
@@ -334,7 +335,7 @@
 done
 
 text{*\noindent
-and then solve our main theorem:
+and then prove our main theorem:
 *}
 
 theorem rev_rev [simp]: "rev(rev xs) = xs";

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -32,12 +32,11 @@
 and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}.
 
 \begin{warn}
-  Syntax annotations are a powerful but completely optional feature. You
+  Syntax annotations are a powerful but optional feature. You
   could drop them from theory \isa{ToyList} and go back to the identifiers
-  \isa{Nil} and \isa{Cons}. However, lists are such a
-  central datatype
-  that their syntax is highly customized. We recommend that novices should
-  not use syntax annotations in their own theories.
+  \isa{Nil} and \isa{Cons}.
+  We recommend that novices avoid using
+  syntax annotations in their own theories.
 \end{warn}
 Next, two functions \isa{app} and \isaindexbold{rev} are declared:%
 \end{isamarkuptext}%
@@ -77,8 +76,8 @@
 % However, this is a subtle issue that we cannot discuss here further.
 
 \begin{warn}
-  As we have indicated, the desire for total functions is not a gratuitously
-  imposed restriction but an essential characteristic of HOL. It is only
+  As we have indicated, the requirement for total functions is not a gratuitous
+  restriction but an essential characteristic of HOL\@. It is only
   because of totality that reasoning in HOL is comparatively easy.  More
   generally, the philosophy in HOL is not to allow arbitrary axioms (such as
   function definitions whose totality has not been proved) because they
@@ -113,7 +112,7 @@
 illustrate not just the basic proof commands but also the typical proof
 process.
 
-\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}}
+\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.}
 
 Our goal is to show that reversing a list twice produces the original
 list. The input line%
@@ -121,6 +120,8 @@
 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \index{*theorem|bold}\index{*simp (attribute)|bold}
+\noindent
+does several things.  It
 \begin{itemize}
 \item
 establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs},
@@ -221,7 +222,7 @@
 \begin{isamarkuptxt}%
 \noindent The keywords \isacommand{theorem}\index{*theorem} and
 \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
-the importance we attach to a proposition. In general, we use the words
+the importance we attach to a proposition.  We use the words
 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
 interchangeably.
 
@@ -320,7 +321,7 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 \noindent
-and then solve our main theorem:%
+and then prove our main theorem:%
 \end{isamarkuptext}%
 \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline

--- a/doc-src/TutorialI/Trie/Trie.thy	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Trie/Trie.thy	Fri Jan 05 18:32:57 2001 +0100
@@ -3,7 +3,7 @@
 (*>*)
 text{*
 To minimize running time, each node of a trie should contain an array that maps
-letters to subtries. We have chosen a (sometimes) more space efficient
+letters to subtries. We have chosen a
 representation where the subtries are held in an association list, i.e.\ a
 list of (letter,trie) pairs.  Abstracting over the alphabet @{typ"'a"} and the
 values @{typ"'v"} we define a trie as follows:
@@ -67,7 +67,7 @@
   "update t (a#as) v =
      (let tt = (case assoc (alist t) a of
                   None \<Rightarrow> Trie None [] | Some at \<Rightarrow> at)
-      in Trie (value t) ((a,update tt as v)#alist t))";
+      in Trie (value t) ((a,update tt as v) # alist t))";
 
 text{*\noindent
 The base case is obvious. In the recursive case the subtrie

--- a/doc-src/TutorialI/Trie/document/Trie.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/Trie/document/Trie.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -4,7 +4,7 @@
 %
 \begin{isamarkuptext}%
 To minimize running time, each node of a trie should contain an array that maps
-letters to subtries. We have chosen a (sometimes) more space efficient
+letters to subtries. We have chosen a
 representation where the subtries are held in an association list, i.e.\ a
 list of (letter,trie) pairs.  Abstracting over the alphabet \isa{{\isacharprime}a} and the
 values \isa{{\isacharprime}v} we define a trie as follows:%
@@ -59,7 +59,7 @@
 \ \ {\isachardoublequote}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline
 \ \ \ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline
-\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}{\isacharhash}alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
+\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}\ {\isacharhash}\ alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 The base case is obvious. In the recursive case the subtrie

--- a/doc-src/TutorialI/basics.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -82,7 +82,7 @@
 \label{sec:TypesTermsForms}
 \indexbold{type}
 
-Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed
+Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed
 logic whose type system resembles that of functional programming languages
 like ML or Haskell. Thus there are
 \begin{description}
@@ -102,7 +102,7 @@
   which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
     \isasymFun~$\tau$}.
 \item[type variables,]\indexbold{type variable}\indexbold{variable!type}
-  denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise
+  denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise
   to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
   function.
 \end{description}
@@ -172,7 +172,7 @@
 \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
 \isa{\isasymnot($t@1$ = $t@2$)}.
 
-The syntax for quantifiers is
+Quantifiers are written as
 \isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and
 \isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}.  There is
 even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
@@ -185,7 +185,7 @@
 \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
 \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed
 in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
-\isa{(x < y)::nat}. The main reason for type constraints are overloaded
+\isa{(x < y)::nat}. The main reason for type constraints is overloading of
 functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for
 a full discussion of overloading and Table~\ref{tab:overloading} for the most
 important overloaded function symbols.
@@ -195,10 +195,10 @@
 functional programming and mathematics. Below we list the main rules that you
 should be familiar with to avoid certain syntactic traps. A particular
 problem for novices can be the priority of operators. If you are unsure, use
-more rather than fewer parentheses. In those cases where Isabelle echoes your
+additional parentheses. In those cases where Isabelle echoes your
 input, you can see which parentheses are dropped---they were superfluous. If
 you are unsure how to interpret Isabelle's output because you don't know
-where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
+where the (dropped) parentheses go, set the \rmindex{flag}
 \isaindexbold{show_brackets}:
 \begin{ttbox}
 ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
@@ -300,4 +300,4 @@
 type each command into the file first and then enter it into Isabelle by
 copy-and-paste, thus ensuring that you have a complete record of your theory.
 As mentioned above, Proof General offers a much superior interface.
-If you have installed Proof General, you can start it with \texttt{Isabelle}.
+If you have installed Proof General, you can start it by typing \texttt{Isabelle}.

--- a/doc-src/TutorialI/fp.tex	Fri Jan 05 18:32:33 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Fri Jan 05 18:32:57 2001 +0100
@@ -29,8 +29,8 @@
 
 {\makeatother\input{ToyList/document/ToyList.tex}}
 
-The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The
-concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs}
+The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The
+concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs}
 constitutes the complete theory \texttt{ToyList} and should reside in file
 \texttt{ToyList.thy}. It is good practice to present all declarations and
 definitions at the beginning of a theory to facilitate browsing.
@@ -159,7 +159,10 @@
 The latter contains many further operations. For example, the functions
 \isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
 element and the remainder of a list. (However, pattern-matching is usually
-preferable to \isa{hd} and \isa{tl}.)  Theory \isa{List} also contains
+preferable to \isa{hd} and \isa{tl}.)  
+Also available are the higher-order
+functions \isa{map}, \isa{filter}, \isa{foldl} and \isa{foldr}.
+Theory \isa{List} also contains
 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
 always use HOL's predefined lists.
@@ -193,7 +196,7 @@
 \isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
 \isa{size} is defined on every datatype, it is overloaded; on lists
 \isa{size} is also called \isaindexbold{length}, which is not overloaded.
-Isbelle will always show \isa{size} on lists as \isa{length}.
+Isabelle will always show \isa{size} on lists as \isa{length}.
 
 
 \subsection{Primitive recursion}
@@ -261,7 +264,7 @@
 \subsection{Type synonyms}
 \indexbold{type synonym}
 
-Type synonyms are similar to those found in ML. Their syntax is fairly self
+Type synonyms are similar to those found in ML\@. Their syntax is fairly self
 explanatory:
 
 \input{Misc/document/types.tex}%
@@ -294,7 +297,7 @@
 \label{sec:Simplification}
 \index{simplification|(}
 
-So far we have proved our theorems by \isa{auto}, which ``simplifies''
+So far we have proved our theorems by \isa{auto}, which simplifies
 \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except
 that it did not need to so far. However, when you go beyond toy examples, you
 need to understand the ingredients of \isa{auto}.  This section covers the
@@ -363,7 +366,8 @@
 \begin{isabelle}
 \isacommand{datatype} t = C "t \isasymRightarrow\ bool"
 \end{isabelle}
-is a real can of worms: in HOL it must be ruled out because it requires a type
+This declaration is a real can of worms.
+In HOL it must be ruled out because it requires a type
 \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
 same cardinality---an impossibility. For the same reason it is not possible
 to allow recursion involving the type \isa{set}, which is isomorphic to
@@ -384,8 +388,10 @@
 \begin{isabelle}
 \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam"
 \end{isabelle}
-do indeed make sense (but note the intentionally different arrow
-\isa{\isasymrightarrow}). There is even a version of LCF on top of HOL,
+do indeed make sense.  Note the different arrow,
+\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow},
+expressing the type of \textbf{continuous} functions. 
+There is even a version of LCF on top of HOL,
 called HOLCF~\cite{MuellerNvOS99}.
 
 \index{*primrec|)}