# HG changeset patch
# User nipkow
# Date 983976851 -3600
# Node ID bb4ede27fcb7d403a5fa8ee639c9d3e4d9f51e54
# Parent  65ede8dfe3041619f77c901554681d53c12dd205
*** empty log message ***

diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -6,7 +6,7 @@
 functions. The best we can do are functions that are
 \emph{underdefined}\index{underdefined function}:
 for certain arguments we only know that a result
-exists, but we don't know what it is. When defining functions that are
+exists, but we do not know what it is. When defining functions that are
 normally considered partial, underdefinedness turns out to be a very
 reasonable alternative.
 
@@ -20,7 +20,6 @@
 
 text{*\noindent
 although it generates a warning.
-
 Even ordinary definitions allow underdefinedness, this time by means of
 preconditions:
 *}
@@ -64,8 +63,9 @@
 As a more substantial example we consider the problem of searching a graph.
 For simplicity our graph is given by a function (@{term f}) of
 type @{typ"'a \<Rightarrow> 'a"} which
-maps each node to its successor, and the task is to find the end of a chain,
-i.e.\ a node pointing to itself. Here is a first attempt:
+maps each node to its successor, i.e.\ the graph is really a tree.
+The task is to find the end of a chain, modelled by a node pointing to
+itself. Here is a first attempt:
 @{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
 This may be viewed as a fixed point finder or as one half of the well known
 \emph{Union-Find} algorithm.
@@ -91,22 +91,24 @@
 The recursion equation itself should be clear enough: it is our aborted
 first attempt augmented with a check that there are no non-trivial loops.
 
-What complicates the termination proof is that the argument of
-@{term find} is a pair. To express the required well-founded relation
-we employ the predefined combinator @{term same_fst} of type
+What complicates the termination proof is that the argument of @{term find}
+is a pair. To express the required well-founded relation we employ the
+predefined combinator @{term same_fst} of type
 @{text[display]"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b\<times>'b)set) \<Rightarrow> (('a\<times>'b) \<times> ('a\<times>'b))set"}
 defined as
 @{thm[display]same_fst_def[no_vars]}
-This combinator is designed for recursive functions on pairs where the first
-component of the argument is passed unchanged to all recursive
-calls. Given a constraint on the first component and a relation on the second
-component, @{term same_fst} builds the required relation on pairs.
-The theorem @{thm[display]wf_same_fst[no_vars]}
-is known to the well-foundedness prover of \isacommand{recdef}.
-Thus well-foundedness of the given relation is immediate.
-Furthermore, each recursive call descends along the given relation:
-the first argument stays unchanged and the second one descends along
-@{term"step1 f"}. The proof merely requires unfolding of some definitions.
+This combinator is designed for
+recursive functions on pairs where the first component of the argument is
+passed unchanged to all recursive calls. Given a constraint on the first
+component and a relation on the second component, @{term same_fst} builds the
+required relation on pairs.  The theorem
+@{thm[display]wf_same_fst[no_vars]}
+is known to the well-foundedness prover of \isacommand{recdef}.  Thus
+well-foundedness of the relation given to \isacommand{recdef} is immediate.
+Furthermore, each recursive call descends along that relation: the first
+argument stays unchanged and the second one descends along @{term"step1
+f"}. The proof merely requires unfolding of some definitions, as specified in
+the \isacommand{hints} above.
 
 Normally you will then derive the following conditional variant of and from
 the recursion equation
@@ -204,7 +206,7 @@
 program. This is in stark contrast to guarded recursion as introduced
 above which requires an explicit test @{prop"x \<in> dom f"} in the
 function body.  Unless @{term dom} is trivial, this leads to a
-definition that is impossible to execute (or prohibitively slow).
+definition that is impossible to execute or prohibitively slow.
 Thus, if you are aiming for an efficiently executable definition
 of a partial function, you are likely to need @{term while}.
 *}
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -32,7 +32,7 @@
 
 Each \isacommand{recdef} definition should be accompanied (after the name of
 the function) by a well-founded relation on the argument type of the
-function.  HOL formalizes some of the most important
+function.  Isabelle/HOL formalizes some of the most important
 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
 example, @{term"measure f"} is always well-founded, and the lexicographic
 product of two well-founded relations is again well-founded, which we relied
@@ -77,7 +77,7 @@
 
 lemma wf_greater: "wf {(i,j). j<i \<and> i \<le> (N::nat)}"
 
-txt{*
+txt{*\noindent
 The proof is by showing that our relation is a subset of another well-founded
 relation: one given by a measure function. 
 *};
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/advanced.tex
--- a/doc-src/TutorialI/Advanced/advanced.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/advanced.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -13,8 +13,8 @@
 \index{*recdef|(}
 
 The purpose of this section is to introduce advanced forms of
-\isacommand{recdef}: how to define recursive function over nested recursive
-datatypes, how to establish termination by means other than measure functions,
+\isacommand{recdef}: how to establish termination by means other than measure
+functions, how to define recursive function over nested recursive datatypes,
 and how to deal with partial functions.
 
 If, after reading this section, you feel that the definition of recursive
@@ -27,16 +27,16 @@
 proof time. In HOL you may have to work hard to define a function, but proofs
 can then proceed unencumbered by worries about undefinedness.
 
+\subsection{Beyond measure}
+\label{sec:beyond-measure}
+\input{Advanced/document/WFrec.tex}
+
 \subsection{Recursion over nested datatypes}
 \label{sec:nested-recdef}
 \input{Recdef/document/Nested0.tex}
 \input{Recdef/document/Nested1.tex}
 \input{Recdef/document/Nested2.tex}
 
-\subsection{Beyond measure}
-\label{sec:beyond-measure}
-\input{Advanced/document/WFrec.tex}
-
 \subsection{Partial functions}
 \index{partial function}
 \input{Advanced/document/Partial.tex}
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/document/Partial.tex
--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -9,7 +9,7 @@
 functions. The best we can do are functions that are
 \emph{underdefined}\index{underdefined function}:
 for certain arguments we only know that a result
-exists, but we don't know what it is. When defining functions that are
+exists, but we do not know what it is. When defining functions that are
 normally considered partial, underdefinedness turns out to be a very
 reasonable alternative.
 
@@ -22,7 +22,6 @@
 \begin{isamarkuptext}%
 \noindent
 although it generates a warning.
-
 Even ordinary definitions allow underdefinedness, this time by means of
 preconditions:%
 \end{isamarkuptext}%
@@ -67,8 +66,9 @@
 As a more substantial example we consider the problem of searching a graph.
 For simplicity our graph is given by a function (\isa{f}) of
 type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} which
-maps each node to its successor, and the task is to find the end of a chain,
-i.e.\ a node pointing to itself. Here is a first attempt:
+maps each node to its successor, i.e.\ the graph is really a tree.
+The task is to find the end of a chain, modelled by a node pointing to
+itself. Here is a first attempt:
 \begin{isabelle}%
 \ \ \ \ \ find\ {\isacharparenleft}f{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find\ {\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}{\isacharparenright}%
 \end{isabelle}
@@ -94,9 +94,9 @@
 The recursion equation itself should be clear enough: it is our aborted
 first attempt augmented with a check that there are no non-trivial loops.
 
-What complicates the termination proof is that the argument of
-\isa{find} is a pair. To express the required well-founded relation
-we employ the predefined combinator \isa{same{\isacharunderscore}fst} of type
+What complicates the termination proof is that the argument of \isa{find}
+is a pair. To express the required well-founded relation we employ the
+predefined combinator \isa{same{\isacharunderscore}fst} of type
 \begin{isabelle}%
 \ \ \ \ \ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b{\isasymtimes}{\isacharprime}b{\isacharparenright}set{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isasymtimes}{\isacharprime}b{\isacharparenright}{\isacharparenright}set%
 \end{isabelle}
@@ -104,18 +104,19 @@
 \begin{isabelle}%
 \ \ \ \ \ same{\isacharunderscore}fst\ P\ R\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}{\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}{\isacharcomma}\ x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x{\isacharprime}\ {\isacharequal}\ x\ {\isasymand}\ P\ x\ {\isasymand}\ {\isacharparenleft}y{\isacharprime}{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ R\ x{\isacharbraceright}%
 \end{isabelle}
-This combinator is designed for recursive functions on pairs where the first
-component of the argument is passed unchanged to all recursive
-calls. Given a constraint on the first component and a relation on the second
-component, \isa{same{\isacharunderscore}fst} builds the required relation on pairs.
-The theorem \begin{isabelle}%
+This combinator is designed for
+recursive functions on pairs where the first component of the argument is
+passed unchanged to all recursive calls. Given a constraint on the first
+component and a relation on the second component, \isa{same{\isacharunderscore}fst} builds the
+required relation on pairs.  The theorem
+\begin{isabelle}%
 \ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ P\ x\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}R\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ wf\ {\isacharparenleft}same{\isacharunderscore}fst\ P\ R{\isacharparenright}%
 \end{isabelle}
-is known to the well-foundedness prover of \isacommand{recdef}.
-Thus well-foundedness of the given relation is immediate.
-Furthermore, each recursive call descends along the given relation:
-the first argument stays unchanged and the second one descends along
-\isa{step{\isadigit{1}}\ f}. The proof merely requires unfolding of some definitions.
+is known to the well-foundedness prover of \isacommand{recdef}.  Thus
+well-foundedness of the relation given to \isacommand{recdef} is immediate.
+Furthermore, each recursive call descends along that relation: the first
+argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof merely requires unfolding of some definitions, as specified in
+the \isacommand{hints} above.
 
 Normally you will then derive the following conditional variant of and from
 the recursion equation%
@@ -213,7 +214,7 @@
 program. This is in stark contrast to guarded recursion as introduced
 above which requires an explicit test \isa{x\ {\isasymin}\ dom\ f} in the
 function body.  Unless \isa{dom} is trivial, this leads to a
-definition that is impossible to execute (or prohibitively slow).
+definition that is impossible to execute or prohibitively slow.
 Thus, if you are aiming for an efficiently executable definition
 of a partial function, you are likely to need \isa{while}.%
 \end{isamarkuptext}%
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -34,7 +34,7 @@
 
 Each \isacommand{recdef} definition should be accompanied (after the name of
 the function) by a well-founded relation on the argument type of the
-function.  HOL formalizes some of the most important
+function.  Isabelle/HOL formalizes some of the most important
 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
 example, \isa{measure\ f} is always well-founded, and the lexicographic
 product of two well-founded relations is again well-founded, which we relied
@@ -74,6 +74,7 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ wf{\isacharunderscore}greater{\isacharcolon}\ {\isachardoublequote}wf\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}j{\isacharparenright}{\isachardot}\ j{\isacharless}i\ {\isasymand}\ i\ {\isasymle}\ {\isacharparenleft}N{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
+\noindent
 The proof is by showing that our relation is a subset of another well-founded
 relation: one given by a measure function.%
 \end{isamarkuptxt}%
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/document/simp.tex
--- a/doc-src/TutorialI/Advanced/document/simp.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -22,7 +22,7 @@
 \begin{isamarkuptext}%
 \label{sec:simp-cong}
 It is hardwired into the simplifier that while simplifying the conclusion $Q$
-of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
+of $P \Imp Q$ it is legal to make uses of the assumption $P$. This
 kind of contextual information can also be made available for other
 operators. For example, \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ xs\ {\isacharat}\ xs\ {\isacharequal}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} when simplifying \isa{xs\ {\isacharat}\ xs\ {\isacharequal}\ xs}. The generation of contextual information during simplification is
 controlled by so-called \bfindex{congruence rules}. This is the one for
@@ -41,8 +41,8 @@
 \ \ \ \ \ {\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isasymrbrakk}\isanewline
 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
 \end{isabelle}
-The congruence rule for conditional expressions supply contextual
-information for simplifying the arms:
+The congruence rule for conditional expressions supplies contextual
+information for simplifying the \isa{then} and \isa{else} cases:
 \begin{isabelle}%
 \ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline
 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}%
@@ -55,7 +55,7 @@
 Only the first argument is simplified; the others remain unchanged.
 This makes simplification much faster and is faithful to the evaluation
 strategy in programming languages, which is why this is the default
-congruence rule for \isa{if}. Analogous rules control the evaluaton of
+congruence rule for \isa{if}. Analogous rules control the evaluation of
 \isa{case} expressions.
 
 You can declare your own congruence rules with the attribute \isa{cong},
@@ -122,7 +122,7 @@
 
 Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely
 necessary because the built-in arithmetic prover often succeeds without
-such hints.%
+such tricks.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{How It Works%
@@ -167,8 +167,7 @@
 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, as they must be
-before the rule can actually be applied.
+introduced conditions may be hard to solve.
   
 There is no restriction on the form of the right-hand
 sides.  They may not contain extraneous term or type variables, though.%
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/simp.thy
--- a/doc-src/TutorialI/Advanced/simp.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/simp.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -17,7 +17,7 @@
 
 text{*\label{sec:simp-cong}
 It is hardwired into the simplifier that while simplifying the conclusion $Q$
-of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
+of $P \Imp Q$ it is legal to make uses of the assumption $P$. This
 kind of contextual information can also be made available for other
 operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
 True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
@@ -33,8 +33,8 @@
 Here are some more examples.  The congruence rules for bounded
 quantifiers supply contextual information about the bound variable:
 @{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
-The congruence rule for conditional expressions supply contextual
-information for simplifying the arms:
+The congruence rule for conditional expressions supplies contextual
+information for simplifying the @{text then} and @{text else} cases:
 @{thm[display]if_cong[no_vars]}
 A congruence rule can also \emph{prevent} simplification of some arguments.
 Here is an alternative congruence rule for conditional expressions:
@@ -42,7 +42,7 @@
 Only the first argument is simplified; the others remain unchanged.
 This makes simplification much faster and is faithful to the evaluation
 strategy in programming languages, which is why this is the default
-congruence rule for @{text if}. Analogous rules control the evaluaton of
+congruence rule for @{text if}. Analogous rules control the evaluation of
 @{text case} expressions.
 
 You can declare your own congruence rules with the attribute @{text cong},
@@ -107,7 +107,7 @@
 
 Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
 necessary because the built-in arithmetic prover often succeeds without
-such hints.
+such tricks.
 *}
 
 subsection{*How It Works*}
@@ -149,8 +149,7 @@
 ?f ?x \<Longrightarrow> ?y \<in> range ?f = 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, as they must be
-before the rule can actually be applied.
+introduced conditions may be hard to solve.
   
 There is no restriction on the form of the right-hand
 sides.  They may not contain extraneous term or type variables, though.
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/CTL/CTLind.thy
--- a/doc-src/TutorialI/CTL/CTLind.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -58,51 +58,53 @@
 expresses.  Simplification shows that this is a path starting with @{term t} 
 and that the instantiated induction hypothesis implies the conclusion.
 
-Now we come to the key lemma. It says that if @{term t} can be reached by a
-finite @{term A}-avoiding path from @{term s}, then @{prop"t \<in> lfp(af A)"},
-provided there is no infinite @{term A}-avoiding path starting from @{term
-s}.
+Now we come to the key lemma. Assuming that no infinite @{term A}-avoiding
+path starts from @{term s}, we want to show @{prop"s \<in> lfp(af A)"}. This
+can be generalized by proving that every point @{term t} ``between''
+@{term s} and @{term A}, i.e.\ all of @{term"Avoid s A"},
+is contained in @{term"lfp(af A)"}:
 *}
 
 lemma Avoid_in_lfp[rule_format(no_asm)]:
   "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
+
 txt{*\noindent
-The trick is not to induct on @{prop"t \<in> Avoid s A"}, as even the base
-case would be a problem, but to proceed by well-founded induction on~@{term
-t}. Hence\hbox{ @{prop"t \<in> Avoid s A"}} must be brought into the conclusion as
-well, which the directive @{text rule_format} undoes at the end (see below).
-But induction with respect to which well-founded relation? The
-one we want is the restriction
-of @{term M} to @{term"Avoid s A"}:
-@{term[display]"{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}"}
+The proof is by induction on the ``distance'' between @{term t} and @{term
+A}. Remember that @{prop"lfp(af A) = A \<union> M\<inverse> `` lfp(af A)"}.
+If @{term t} is already in @{term A}, then @{prop"t \<in> lfp(af A)"} is
+trivial. If @{term t} is not in @{term A} but all successors are in
+@{term"lfp(af A)"} (induction hypothesis), then @{prop"t \<in> lfp(af A)"} is
+again trivial.
+
+The formal counterpart of this proof sketch is a well-founded induction
+w.r.t.\ @{term M} restricted to (roughly speaking) @{term"Avoid s A - A"}:
+@{term[display]"{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}"}
 As we shall see in a moment, the absence of infinite @{term A}-avoiding paths
 starting from @{term s} implies well-foundedness of this relation. For the
 moment we assume this and proceed with the induction:
 *}
 
-apply(subgoal_tac
-  "wf{(y,x). (x,y)\<in>M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}");
+apply(subgoal_tac "wf{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}");
  apply(erule_tac a = t in wf_induct);
  apply(clarsimp);
+(*<*)apply(rename_tac t)(*>*)
 
 txt{*\noindent
 @{subgoals[display,indent=0,margin=65]}
-\REMARK{I put in this proof state but I wonder if readers will be able to
-follow this proof. You could prove that your relation is WF in a 
-lemma beforehand, maybe omitting that proof.}
 Now the induction hypothesis states that if @{prop"t \<notin> A"}
 then all successors of @{term t} that are in @{term"Avoid s A"} are in
-@{term"lfp (af A)"}. To prove the actual goal we unfold @{term lfp} once. Now
-we have to prove that @{term t} is in @{term A} or all successors of @{term
-t} are in @{term"lfp (af A)"}. If @{term t} is not in @{term A}, the second
+@{term"lfp (af A)"}. Unfolding @{term lfp} in the conclusion of the first
+subgoal once, we have to prove that @{term t} is in @{term A} or all successors
+of @{term t} are in @{term"lfp (af A)"}: if @{term t} is not in @{term A},
+the second 
 @{term Avoid}-rule implies that all successors of @{term t} are in
 @{term"Avoid s A"} (because we also assume @{prop"t \<in> Avoid s A"}), and
 hence, by the induction hypothesis, all successors of @{term t} are indeed in
 @{term"lfp(af A)"}. Mechanically:
 *}
 
- apply(rule ssubst [OF lfp_unfold[OF mono_af]]);
- apply(simp only: af_def);
+ apply(subst lfp_unfold[OF mono_af]);
+ apply(simp (no_asm) add: af_def);
  apply(blast intro:Avoid.intros);
 
 txt{*
@@ -124,7 +126,8 @@
 done
 
 text{*
-The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive means
+The @{text"(no_asm)"} modifier of the @{text"rule_format"} directive in the
+statement of the lemma means
 that the assumption is left unchanged --- otherwise the @{text"\<forall>p"} is turned
 into a @{text"\<And>p"}, which would complicate matters below. As it is,
 @{thm[source]Avoid_in_lfp} is now
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/CTL/document/CTLind.tex
--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -58,56 +58,57 @@
 expresses.  Simplification shows that this is a path starting with \isa{t} 
 and that the instantiated induction hypothesis implies the conclusion.
 
-Now we come to the key lemma. It says that if \isa{t} can be reached by a
-finite \isa{A}-avoiding path from \isa{s}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}},
-provided there is no infinite \isa{A}-avoiding path starting from \isa{s}.%
+Now we come to the key lemma. Assuming that no infinite \isa{A}-avoiding
+path starts from \isa{s}, we want to show \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. This
+can be generalized by proving that every point \isa{t} ``between''
+\isa{s} and \isa{A}, i.e.\ all of \isa{Avoid\ s\ A},
+is contained in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequote}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\ t\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ t\ {\isasymin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
-The trick is not to induct on \isa{t\ {\isasymin}\ Avoid\ s\ A}, as even the base
-case would be a problem, but to proceed by well-founded induction on~\isa{t}. Hence\hbox{ \isa{t\ {\isasymin}\ Avoid\ s\ A}} must be brought into the conclusion as
-well, which the directive \isa{rule{\isacharunderscore}format} undoes at the end (see below).
-But induction with respect to which well-founded relation? The
-one we want is the restriction
-of \isa{M} to \isa{Avoid\ s\ A}:
+The proof is by induction on the ``distance'' between \isa{t} and \isa{A}. Remember that \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ A\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
+If \isa{t} is already in \isa{A}, then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
+trivial. If \isa{t} is not in \isa{A} but all successors are in
+\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}} (induction hypothesis), then \isa{t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}} is
+again trivial.
+
+The formal counterpart of this proof sketch is a well-founded induction
+w.r.t.\ \isa{M} restricted to (roughly speaking) \isa{Avoid\ s\ A\ {\isacharminus}\ A}:
 \begin{isabelle}%
-\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
+\ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
 \end{isabelle}
 As we shall see in a moment, the absence of infinite \isa{A}-avoiding paths
 starting from \isa{s} implies well-foundedness of this relation. For the
 moment we assume this and proceed with the induction:%
 \end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\isanewline
-\ \ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}wf{\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}{\isachardoublequote}{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ x\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ \ \ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isasymrbrakk}\isanewline
-\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }{\isasymLongrightarrow}\ x\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ {\isasymlbrakk}{\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharsemicolon}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ }{\isasymforall}y{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ A\ {\isasymlongrightarrow}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ \ \ \ {\isasymforall}y{\isachardot}\ }y\ {\isasymin}\ Avoid\ s\ A\ {\isasymlongrightarrow}\ y\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isasymrbrakk}\isanewline
+\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}t{\isachardot}\ }{\isasymLongrightarrow}\ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
 \ {\isadigit{2}}{\isachardot}\ {\isasymforall}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A\ {\isasymLongrightarrow}\isanewline
-\isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\isanewline
-\isaindent{\ {\isadigit{2}}{\isachardot}\ wf\ \ }{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ y\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
+\isaindent{\ {\isadigit{2}}{\isachardot}\ }wf\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ x\ {\isasymin}\ Avoid\ s\ A\ {\isasymand}\ x\ {\isasymnotin}\ A{\isacharbraceright}%
 \end{isabelle}
-\REMARK{I put in this proof state but I wonder if readers will be able to
-follow this proof. You could prove that your relation is WF in a 
-lemma beforehand, maybe omitting that proof.}
 Now the induction hypothesis states that if \isa{t\ {\isasymnotin}\ A}
 then all successors of \isa{t} that are in \isa{Avoid\ s\ A} are in
-\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. To prove the actual goal we unfold \isa{lfp} once. Now
-we have to prove that \isa{t} is in \isa{A} or all successors of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. If \isa{t} is not in \isa{A}, the second
+\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Unfolding \isa{lfp} in the conclusion of the first
+subgoal once, we have to prove that \isa{t} is in \isa{A} or all successors
+of \isa{t} are in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}: if \isa{t} is not in \isa{A},
+the second 
 \isa{Avoid}-rule implies that all successors of \isa{t} are in
 \isa{Avoid\ s\ A} (because we also assume \isa{t\ {\isasymin}\ Avoid\ s\ A}), and
 hence, by the induction hypothesis, all successors of \isa{t} are indeed in
 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Mechanically:%
 \end{isamarkuptxt}%
-\ \isacommand{apply}{\isacharparenleft}rule\ ssubst\ {\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}%
 \begin{isamarkuptxt}%
 Having proved the main goal we return to the proof obligation that the above
@@ -127,7 +128,8 @@
 \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
 \isacommand{done}%
 \begin{isamarkuptext}%
-The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive means
+The \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}} modifier of the \isa{rule{\isacharunderscore}format} directive in the
+statement of the lemma means
 that the assumption is left unchanged --- otherwise the \isa{{\isasymforall}p} is turned
 into a \isa{{\isasymAnd}p}, which would complicate matters below. As it is,
 \isa{Avoid{\isacharunderscore}in{\isacharunderscore}lfp} is now
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -62,33 +62,26 @@
 This time, induction leaves us with a trivial base case:
 @{subgoals[display,indent=0,goals_limit=1]}
 And @{text"auto"} completes the proof.
-*}
-(*<*)
-by auto;
-(*>*)
 
-
-text{*
 If there are multiple premises $A@1$, \dots, $A@n$ containing the
 induction variable, you should turn the conclusion $C$ into
 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
-(see the remark?? in \S\ref{??}).
 Additionally, you may also have to universally quantify some other variables,
-which can yield a fairly complex conclusion.  However, @{text"rule_format"} 
+which can yield a fairly complex conclusion.  However, @{text rule_format} 
 can remove any number of occurrences of @{text"\<forall>"} and
 @{text"\<longrightarrow>"}.
-
-Here is a simple example (which is proved by @{text"blast"}):
-*};
+*}
 
+(*<*)
+by auto;
+(*>*)
+(*
+Here is a simple example (which is proved by @{text"blast"}):
 lemma simple[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
-(*<*)
 by blast;
-(*>*)
+*)
 
 text{*
-\medskip
-
 A second reason why your proposition may not be amenable to induction is that
 you want to induct on a whole term, rather than an individual variable. In
 general, when inducting on some term $t$ you must rephrase the conclusion $C$
@@ -133,7 +126,7 @@
 
 text{*\noindent
 The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
-be proved by induction on @{term"f n"}. Following the recipe outlined
+be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:
 *};
 
@@ -155,19 +148,16 @@
 the other case:
 *}
 
-apply(rule allI);
-apply(case_tac i);
- apply(simp);
-
+apply(rule allI)
+apply(case_tac i)
+ apply(simp)
 txt{*
 @{subgoals[display,indent=0]}
-*};
-
-by(blast intro!: f_ax Suc_leI intro: le_less_trans);
+*}
+by(blast intro!: f_ax Suc_leI intro: le_less_trans)
 
 text{*\noindent
-If you find the last step puzzling, here are the 
-two other lemmas used above:
+If you find the last step puzzling, here are the two lemmas it employs:
 \begin{isabelle}
 @{thm Suc_leI[no_vars]}
 \rulename{Suc_leI}\isanewline
@@ -193,7 +183,7 @@
 Chapter~\ref{sec:part2?} introduces a language for writing readable
 proofs.
 
-We can now derive the desired @{prop"i <= f i"} from @{text"f_incr"}:
+We can now derive the desired @{prop"i <= f i"} from @{thm[source]f_incr_lem}:
 *};
 
 lemmas f_incr = f_incr_lem[rule_format, OF refl];
@@ -256,17 +246,16 @@
 apply(induct_tac n);
 
 txt{*\noindent
-The base case is trivially true. For the induction step (@{prop"m <
+The base case is vacuously true. For the induction step (@{prop"m <
 Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
 hypothesis and case @{prop"m = n"} follows from the assumption, again using
 the induction hypothesis:
 *};
-apply(blast);
+ apply(blast);
 by(blast elim:less_SucE)
 
 text{*\noindent
-The elimination rule @{thm[source]less_SucE} expresses the case distinction
-mentioned above:
+The elimination rule @{thm[source]less_SucE} expresses the case distinction:
 @{thm[display]"less_SucE"[no_vars]}
 
 Now it is straightforward to derive the original version of
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -63,25 +63,18 @@
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ hd\ {\isacharparenleft}rev\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ last\ {\isacharbrackleft}{\isacharbrackright}%
 \end{isabelle}
-And \isa{auto} completes the proof.%
-\end{isamarkuptxt}%
-%
-\begin{isamarkuptext}%
+And \isa{auto} completes the proof.
+
 If there are multiple premises $A@1$, \dots, $A@n$ containing the
 induction variable, you should turn the conclusion $C$ into
 \[ A@1 \longrightarrow \cdots A@n \longrightarrow C \]
-(see the remark?? in \S\ref{??}).
 Additionally, you may also have to universally quantify some other variables,
 which can yield a fairly complex conclusion.  However, \isa{rule{\isacharunderscore}format} 
 can remove any number of occurrences of \isa{{\isasymforall}} and
-\isa{{\isasymlongrightarrow}}.
-
-Here is a simple example (which is proved by \isa{blast}):%
-\end{isamarkuptext}%
-\isacommand{lemma}\ simple{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
+\isa{{\isasymlongrightarrow}}.%
+\end{isamarkuptxt}%
+%
 \begin{isamarkuptext}%
-\medskip
-
 A second reason why your proposition may not be amenable to induction is that
 you want to induct on a whole term, rather than an individual variable. In
 general, when inducting on some term $t$ you must rephrase the conclusion $C$
@@ -129,7 +122,7 @@
 \begin{isamarkuptext}%
 \noindent
 The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
-be proved by induction on \isa{f\ n}. Following the recipe outlined
+be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
@@ -164,8 +157,7 @@
 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharbang}{\isacharcolon}\ f{\isacharunderscore}ax\ Suc{\isacharunderscore}leI\ intro{\isacharcolon}\ le{\isacharunderscore}less{\isacharunderscore}trans{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-If you find the last step puzzling, here are the 
-two other lemmas used above:
+If you find the last step puzzling, here are the two lemmas it employs:
 \begin{isabelle}
 \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
 \rulename{Suc_leI}\isanewline
@@ -191,7 +183,7 @@
 Chapter~\ref{sec:part2?} introduces a language for writing readable
 proofs.
 
-We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr}:%
+We can now derive the desired \isa{i\ {\isasymle}\ f\ i} from \isa{f{\isacharunderscore}incr{\isacharunderscore}lem}:%
 \end{isamarkuptext}%
 \isacommand{lemmas}\ f{\isacharunderscore}incr\ {\isacharequal}\ f{\isacharunderscore}incr{\isacharunderscore}lem{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}%
 \begin{isamarkuptext}%
@@ -253,16 +245,15 @@
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-The base case is trivially true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction
+The base case is vacuously true. For the induction step (\isa{m\ {\isacharless}\ Suc\ n}) we distinguish two cases: case \isa{m\ {\isacharless}\ n} is true by induction
 hypothesis and case \isa{m\ {\isacharequal}\ n} follows from the assumption, again using
 the induction hypothesis:%
 \end{isamarkuptxt}%
-\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
 \isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}%
 \begin{isamarkuptext}%
 \noindent
-The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction
-mentioned above:
+The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
 \begin{isabelle}%
 \ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
 \end{isabelle}
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Recdef/Nested0.thy
--- a/doc-src/TutorialI/Recdef/Nested0.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested0.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -13,7 +13,7 @@
 of primitive recursive functions leads to overly verbose definitions. Moreover,
 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
 you needed to declare essentially the same function as @{term"rev"}
-and prove many standard properties of list reverse all over again. 
+and prove many standard properties of list reversal all over again. 
 We will now show you how \isacommand{recdef} can simplify
 definitions and proofs about nested recursive datatypes. As an example we
 choose exercise~\ref{ex:trev-trev}:
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -1,17 +1,15 @@
 (*<*)
-theory Nested2 = Nested0:;
+theory Nested2 = Nested0:
 (*>*)
 
-text{*\noindent
-The termintion condition is easily proved by induction:
-*};
+text{*The termintion condition is easily proved by induction:*}
 
-lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)";
-by(induct_tac ts, auto);
+lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"
+by(induct_tac ts, auto)
 (*<*)
 recdef trev "measure size"
  "trev (Var x) = Var x"
- "trev (App f ts) = App f (rev(map trev ts))";
+ "trev (App f ts) = App f (rev(map trev ts))"
 (*>*)
 text{*\noindent
 By making this theorem a simplification rule, \isacommand{recdef}
@@ -20,17 +18,16 @@
 lemma directly.  We no longer need the verbose
 induction schema for type @{text"term"} and can use the simpler one arising from
 @{term"trev"}:
-*};
+*}
 
-lemma "trev(trev t) = t";
-apply(induct_tac t rule:trev.induct);
-txt{*\noindent
-This leaves us with a trivial base case @{term"trev (trev (Var x)) = Var x"} and the step case
-@{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"}
-both of which are solved by simplification:
-*};
+lemma "trev(trev t) = t"
+apply(induct_tac t rule:trev.induct)
+txt{*
+@{subgoals[display,indent=0]}
+Both the base case and the induction step fall to simplification:
+*}
 
-by(simp_all add:rev_map sym[OF map_compose] cong:map_cong);
+by(simp_all add:rev_map sym[OF map_compose] cong:map_cong)
 
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend that you go through
@@ -83,7 +80,7 @@
 by giving them the \isaindexbold{recdef_cong} attribute as in
 *}
 
-declare map_cong[recdef_cong];
+declare map_cong[recdef_cong]
 
 text{*
 Note that the @{text cong} and @{text recdef_cong} attributes are
@@ -94,5 +91,5 @@
 %The simplifier's congruence rules cannot be used by recdef.
 %For example the weak congruence rules for if and case would prevent
 %recdef from generating sensible termination conditions.
-*};
-(*<*)end;(*>*)
+*}
+(*<*)end(*>*)
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Recdef/document/Nested0.tex
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -12,7 +12,7 @@
 of primitive recursive functions leads to overly verbose definitions. Moreover,
 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
 you needed to declare essentially the same function as \isa{rev}
-and prove many standard properties of list reverse all over again. 
+and prove many standard properties of list reversal all over again. 
 We will now show you how \isacommand{recdef} can simplify
 definitions and proofs about nested recursive datatypes. As an example we
 choose exercise~\ref{ex:trev-trev}:%
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -3,7 +3,6 @@
 \def\isabellecontext{Nested{\isadigit{2}}}%
 %
 \begin{isamarkuptext}%
-\noindent
 The termintion condition is easily proved by induction:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline
@@ -20,13 +19,13 @@
 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
 \begin{isamarkuptxt}%
-\noindent
-This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
 \begin{isabelle}%
-\ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
-\isaindent{\ \ \ \ \ }trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}f\ ts{\isachardot}\isanewline
+\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymforall}x{\isachardot}\ x\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ x{\isacharparenright}\ {\isacharequal}\ x\ {\isasymLongrightarrow}\isanewline
+\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
 \end{isabelle}
-both of which are solved by simplification:%
+Both the base case and the induction step fall to simplification:%
 \end{isamarkuptxt}%
 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}%
 \begin{isamarkuptext}%
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/Axioms.thy
--- a/doc-src/TutorialI/Types/Axioms.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -30,9 +30,9 @@
 @{thm[show_sorts]refl}.
 
 We have not made @{thm[source]less_le} a global definition because it would
-fix once and for all that @{text"<<"} is defined in terms of @{text"<<="}.
-There are however situations where it is the other way around, which such a
-definition would complicate. The slight drawback of the above class is that
+fix once and for all that @{text"<<"} is defined in terms of @{text"<<="} and
+never the other way around. Below you will see why we want to avoid this
+asymmetry. The drawback of the above class is that
 we need to define both @{text"<<="} and @{text"<<"} for each instance.
 
 We can now prove simple theorems in this abstract setting, for example
@@ -85,8 +85,8 @@
 
 text{*\noindent
 The effect is not stunning, but it demonstrates the principle.  It also shows
-that tools like the simplifier can deal with generic rules as well. Moreover,
-it should be clear that the main advantage of the axiomatic method is that
+that tools like the simplifier can deal with generic rules as well.
+It should be clear that the main advantage of the axiomatic method is that
 theorems can be proved in the abstract and one does not need to repeat the
 proof for each instance.
 *}
@@ -97,17 +97,17 @@
 \emph{linear} or \emph{total} order: *}
 
 axclass linord < parord
-total: "x <<= y \<or> y <<= x"
+linear: "x <<= y \<or> y <<= x"
 
 text{*\noindent
 By construction, @{text linord} inherits all axioms from @{text parord}.
-Therefore we can show that totality can be expressed in terms of @{text"<<"}
+Therefore we can show that linearity can be expressed in terms of @{text"<<"}
 as follows:
 *}
 
-lemma "\<And>x::'a::linord. x<<y \<or> x=y \<or> y<<x";
+lemma "\<And>x::'a::linord. x << y \<or> x = y \<or> y << x";
 apply(simp add: less_le);
-apply(insert total);
+apply(insert linear);
 apply blast;
 done
 
@@ -133,13 +133,20 @@
 text{*\noindent
 It is well known that partial orders are the same as strict orders. Let us
 prove one direction, namely that partial orders are a subclass of strict
-orders. The proof follows the ususal pattern: *}
+orders. *}
 
 instance parord < strord
 apply intro_classes;
-apply(simp_all (no_asm_use) add:less_le);
-  apply(blast intro: trans antisym);
- apply(blast intro: refl);
+
+txt{*\noindent
+@{subgoals[display,show_sorts]}
+Assuming @{text"'a :: parord"}, the three axioms of class @{text strord}
+are easily proved:
+*}
+
+  apply(simp_all (no_asm_use) add:less_le);
+ apply(blast intro: trans antisym);
+apply(blast intro: refl);
 done
 
 text{*
@@ -207,7 +214,7 @@
 represents the intersection of the $C@i$. Such an expression is called a
 \bfindex{sort}, and sorts can appear in most places where we have only shown
 classes so far, for example in type constraints: @{text"'a::{linord,wford}"}.
-In fact, @{text"'a::ord"} is short for @{text"'a::{ord}"}.
+In fact, @{text"'a::C"} is short for @{text"'a::{C}"}.
 However, we do not pursue this rarefied concept further.
 
 This concludes our demonstration of type classes based on orderings.  We
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/Overloading.thy
--- a/doc-src/TutorialI/Types/Overloading.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -16,12 +16,4 @@
   "xs <<= (ys::'a::ordrel list)  \<equiv>  \<exists>zs. ys = xs@zs"
 strict_prefix_def:
   "xs << (ys::'a::ordrel list)   \<equiv>  xs <<= ys \<and> xs \<noteq> ys"
-  
-text{*
-We could also have made the second definition non-overloaded once and for
-all: @{prop"x << y \<equiv> x <<= y \<and> x \<noteq> y"}.  This would have saved us writing
-many similar definitions at different types, but it would also have fixed
-that @{text <<} is defined in terms of @{text <<=} and never the other way
-around. Below you will see why we want to avoid this asymmetry.
-*}
 (*<*)end(*>*)
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/Overloading0.thy
--- a/doc-src/TutorialI/Types/Overloading0.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading0.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -27,17 +27,17 @@
 common instance. What is more, the recursion in @{thm[source]inverse_pair} is
 benign because the type of @{term[source]inverse} becomes smaller: on the
 left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
-@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"(overloaded)"} tells Isabelle that
+@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"("}\isacommand{overloaded}@{text")"} tells Isabelle that
 the definitions do intentionally define @{term[source]inverse} only at
 instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely supresses
 warnings to that effect.
 
 However, there is nothing to prevent the user from forming terms such as
-@{term[source]"inverse []"} and proving theorems as @{prop[source]"inverse []
+@{text"inverse []"} and proving theorems as @{text"inverse []
 = inverse []"}, although we never defined inverse on lists. We hasten to say
 that there is nothing wrong with such terms and theorems. But it would be
 nice if we could prevent their formation, simply because it is very likely
-that the user did not mean to write what he did. Thus he had better not waste
-his time pursuing it further. This requires the use of type classes.
+that the user did not mean to write what he did. Thus she had better not waste
+her time pursuing it further. This requires the use of type classes.
 *}
 (*<*)end(*>*)
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/Overloading2.thy
--- a/doc-src/TutorialI/Types/Overloading2.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -29,8 +29,8 @@
 In addition there is a special input syntax for bounded quantifiers:
 \begin{center}
 \begin{tabular}{lcl}
-@{text"\<forall>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\
-@{text"\<exists>x \<le> y. P x"} & @{text"\<equiv>"} & @{prop"\<exists>x. x \<le> y \<and> P x"}
+@{text"\<forall>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<forall>x. x \<le> y \<longrightarrow> P x"} \\
+@{text"\<exists>x \<le> y. P x"} & @{text"\<rightharpoonup>"} & @{prop"\<exists>x. x \<le> y \<and> P x"}
 \end{tabular}
 \end{center}
 And analogously for @{text"<"} instead of @{text"\<le>"}.
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/Typedef.thy
--- a/doc-src/TutorialI/Types/Typedef.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedef.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -3,12 +3,11 @@
 section{*Introducing New Types*}
 
 text{*\label{sec:adv-typedef}
-By now we have seen a number of ways for introducing new types, for example
-type synonyms, recursive datatypes and records. For most applications, this
-repertoire should be quite sufficient. Very occasionally you may feel the
-need for a more advanced type. If you cannot do without that type, and you are
-certain that it is not definable by any of the standard means,
-then read on.
+For most applications, a combination of predefined types like @{typ bool} and
+@{text"\<Rightarrow>"} with recursive datatypes and records is quite sufficient. Very
+occasionally you may feel the need for a more advanced type. If you cannot do
+without that type, and you are certain that it is not definable by any of the
+standard means, then read on.
 \begin{warn}
   Types in HOL must be non-empty; otherwise the quantifier rules would be
   unsound, because $\exists x.\ x=x$ is a theorem.
@@ -34,8 +33,7 @@
 
 In principle we can always get rid of such type declarations by making those
 types parameters of every other type, thus keeping the theory generic. In
-practice, however, the resulting clutter can sometimes make types hard to
-read.
+practice, however, the resulting clutter can make types hard to read.
 
 If you are looking for a quick and dirty way of introducing a new type
 together with its properties: declare the type and state its properties as
@@ -49,7 +47,7 @@
 However, we strongly discourage this approach, except at explorative stages
 of your development. It is extremely easy to write down contradictory sets of
 axioms, in which case you will be able to prove everything but it will mean
-nothing.  Here the axiomatic approach is
+nothing.  In the example above, the axiomatic approach is
 unnecessary: a one-element type called @{typ unit} is already defined in HOL.
 *}
 
@@ -63,7 +61,7 @@
 a type definition is merely a notational device: you introduce a new name for
 a subset of an existing type. This does not add any logical power to HOL,
 because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become undigestible
+type. However, the resulting theories could easily become indigestible
 because instead of implicit types you would have explicit sets in your
 formulae.
 
@@ -85,7 +83,7 @@
 
 text{*
 This type definition introduces the new type @{typ three} and asserts
-that it is a \emph{copy} of the set @{term"{0,1,2}"}. This assertion
+that it is a copy of the set @{term"{0,1,2}"}. This assertion
 is expressed via a bijection between the \emph{type} @{typ three} and the
 \emph{set} @{term"{0,1,2}"}. To this end, the command declares the following
 constants behind the scenes:
@@ -96,7 +94,7 @@
 @{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
 \end{tabular}
 \end{center}
-Constant @{term three} is explicitly defined as the representing set:
+where constant @{term three} is explicitly defined as the representing set:
 \begin{center}
 @{thm three_def}\hfill(@{thm[source]three_def})
 \end{center}
@@ -233,7 +231,7 @@
 txt{*\noindent
 This substitution step worked nicely because there was just a single
 occurrence of a term of type @{typ three}, namely @{term x}.
-When we now apply the lemma, @{term Q} becomes @{term"\<lambda>n. P(Abs_three
+When we now apply @{thm[source]cases_lemma}, @{term Q} becomes @{term"\<lambda>n. P(Abs_three
 n)"} because @{term"Rep_three x"} is the only term of type @{typ nat}:
 *}
 
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/document/Axioms.tex
--- a/doc-src/TutorialI/Types/document/Axioms.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -33,9 +33,9 @@
 \isa{{\isacharparenleft}{\isacharquery}x{\isasymColon}{\isacharquery}{\isacharprime}a{\isasymColon}parord{\isacharparenright}\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharquery}x}.
 
 We have not made \isa{less{\isacharunderscore}le} a global definition because it would
-fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}}.
-There are however situations where it is the other way around, which such a
-definition would complicate. The slight drawback of the above class is that
+fix once and for all that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
+never the other way around. Below you will see why we want to avoid this
+asymmetry. The drawback of the above class is that
 we need to define both \isa{{\isacharless}{\isacharless}{\isacharequal}} and \isa{{\isacharless}{\isacharless}} for each instance.
 
 We can now prove simple theorems in this abstract setting, for example
@@ -89,8 +89,8 @@
 \begin{isamarkuptext}%
 \noindent
 The effect is not stunning, but it demonstrates the principle.  It also shows
-that tools like the simplifier can deal with generic rules as well. Moreover,
-it should be clear that the main advantage of the axiomatic method is that
+that tools like the simplifier can deal with generic rules as well.
+It should be clear that the main advantage of the axiomatic method is that
 theorems can be proved in the abstract and one does not need to repeat the
 proof for each instance.%
 \end{isamarkuptext}%
@@ -103,16 +103,16 @@
 \emph{linear} or \emph{total} order:%
 \end{isamarkuptext}%
 \isacommand{axclass}\ linord\ {\isacharless}\ parord\isanewline
-total{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}%
+linear{\isacharcolon}\ {\isachardoublequote}x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}{\isacharequal}\ x{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
 By construction, \isa{linord} inherits all axioms from \isa{parord}.
-Therefore we can show that totality can be expressed in terms of \isa{{\isacharless}{\isacharless}}
+Therefore we can show that linearity can be expressed in terms of \isa{{\isacharless}{\isacharless}}
 as follows:%
 \end{isamarkuptext}%
-\isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x{\isacharless}{\isacharless}y\ {\isasymor}\ x{\isacharequal}y\ {\isasymor}\ y{\isacharless}{\isacharless}x{\isachardoublequote}\isanewline
+\isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}x{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}linord{\isachardot}\ x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y\ {\isasymor}\ y\ {\isacharless}{\isacharless}\ x{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
-\isacommand{apply}{\isacharparenleft}insert\ total{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}insert\ linear{\isacharparenright}\isanewline
 \isacommand{apply}\ blast\isanewline
 \isacommand{done}%
 \begin{isamarkuptext}%
@@ -137,13 +137,25 @@
 \noindent
 It is well known that partial orders are the same as strict orders. Let us
 prove one direction, namely that partial orders are a subclass of strict
-orders. The proof follows the ususal pattern:%
+orders.%
 \end{isamarkuptext}%
 \isacommand{instance}\ parord\ {\isacharless}\ strord\isanewline
-\isacommand{apply}\ intro{\isacharunderscore}classes\isanewline
-\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}less{\isacharunderscore}le{\isacharparenright}\isanewline
-\ \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
-\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
+\isacommand{apply}\ intro{\isacharunderscore}classes%
+\begin{isamarkuptxt}%
+\noindent
+\begin{isabelle}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymnot}\ x\ {\isacharless}{\isacharless}\ x\isanewline
+\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharparenleft}y{\isasymColon}{\isacharprime}a{\isacharparenright}\ z{\isasymColon}{\isacharprime}a{\isachardot}\ {\isasymlbrakk}x\ {\isacharless}{\isacharless}\ y{\isacharsemicolon}\ y\ {\isacharless}{\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}{\isacharless}\ z\isanewline
+\ {\isadigit{3}}{\isachardot}\ {\isasymAnd}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}a{\isachardot}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}{\isacharequal}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharless}{\isacharless}\ y\ {\isasymor}\ x\ {\isacharequal}\ y{\isacharparenright}\isanewline
+type\ variables{\isacharcolon}\isanewline
+\isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord%
+\end{isabelle}
+Assuming \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord}
+are easily proved:%
+\end{isamarkuptxt}%
+\ \ \isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}less{\isacharunderscore}le{\isacharparenright}\isanewline
+\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ refl{\isacharparenright}\isanewline
 \isacommand{done}%
 \begin{isamarkuptext}%
 The subclass relation must always be acyclic. Therefore Isabelle will
@@ -194,7 +206,7 @@
 represents the intersection of the $C@i$. Such an expression is called a
 \bfindex{sort}, and sorts can appear in most places where we have only shown
 classes so far, for example in type constraints: \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}linord{\isacharcomma}wford{\isacharbraceright}}.
-In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}ord} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}ord{\isacharbraceright}}.
+In fact, \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}C} is short for \isa{{\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}C{\isacharbraceright}}.
 However, we do not pursue this rarefied concept further.
 
 This concludes our demonstration of type classes based on orderings.  We
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/document/Overloading.tex
--- a/doc-src/TutorialI/Types/document/Overloading.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -15,15 +15,7 @@
 prefix{\isacharunderscore}def{\isacharcolon}\isanewline
 \ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
 strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}%
-\begin{isamarkuptext}%
-We could also have made the second definition non-overloaded once and for
-all: \isa{x\ {\isacharless}{\isacharless}\ y\ {\isasymequiv}\ x\ {\isacharless}{\isacharless}{\isacharequal}\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y}.  This would have saved us writing
-many similar definitions at different types, but it would also have fixed
-that \isa{{\isacharless}{\isacharless}} is defined in terms of \isa{{\isacharless}{\isacharless}{\isacharequal}} and never the other way
-around. Below you will see why we want to avoid this asymmetry.%
-\end{isamarkuptext}%
-\end{isabellebody}%
+\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/document/Overloading0.tex
--- a/doc-src/TutorialI/Types/document/Overloading0.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -31,17 +31,17 @@
 common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
 benign because the type of \isa{inverse} becomes smaller: on the
 left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and
-\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that
+\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\isacharparenright}} tells Isabelle that
 the definitions do intentionally define \isa{inverse} only at
 instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses
 warnings to that effect.
 
 However, there is nothing to prevent the user from forming terms such as
-\isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}} and proving theorems as \isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}, although we never defined inverse on lists. We hasten to say
+\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, although we never defined inverse on lists. We hasten to say
 that there is nothing wrong with such terms and theorems. But it would be
 nice if we could prevent their formation, simply because it is very likely
-that the user did not mean to write what he did. Thus he had better not waste
-his time pursuing it further. This requires the use of type classes.%
+that the user did not mean to write what he did. Thus she had better not waste
+her time pursuing it further. This requires the use of type classes.%
 \end{isamarkuptext}%
 \end{isabellebody}%
 %%% Local Variables:
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/document/Overloading2.tex
--- a/doc-src/TutorialI/Types/document/Overloading2.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -31,8 +31,8 @@
 In addition there is a special input syntax for bounded quantifiers:
 \begin{center}
 \begin{tabular}{lcl}
-\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
-\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymequiv}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
+\isa{{\isasymforall}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymforall}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymlongrightarrow}\ P\ x} \\
+\isa{{\isasymexists}x\ {\isasymle}\ y{\isachardot}\ P\ x} & \isa{{\isasymrightharpoonup}} & \isa{{\isasymexists}x{\isachardot}\ x\ {\isasymle}\ y\ {\isasymand}\ P\ x}
 \end{tabular}
 \end{center}
 And analogously for \isa{{\isacharless}} instead of \isa{{\isasymle}}.
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/document/Typedef.tex
--- a/doc-src/TutorialI/Types/document/Typedef.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -7,12 +7,11 @@
 %
 \begin{isamarkuptext}%
 \label{sec:adv-typedef}
-By now we have seen a number of ways for introducing new types, for example
-type synonyms, recursive datatypes and records. For most applications, this
-repertoire should be quite sufficient. Very occasionally you may feel the
-need for a more advanced type. If you cannot do without that type, and you are
-certain that it is not definable by any of the standard means,
-then read on.
+For most applications, a combination of predefined types like \isa{bool} and
+\isa{{\isasymRightarrow}} with recursive datatypes and records is quite sufficient. Very
+occasionally you may feel the need for a more advanced type. If you cannot do
+without that type, and you are certain that it is not definable by any of the
+standard means, then read on.
 \begin{warn}
   Types in HOL must be non-empty; otherwise the quantifier rules would be
   unsound, because $\exists x.\ x=x$ is a theorem.
@@ -40,8 +39,7 @@
 
 In principle we can always get rid of such type declarations by making those
 types parameters of every other type, thus keeping the theory generic. In
-practice, however, the resulting clutter can sometimes make types hard to
-read.
+practice, however, the resulting clutter can make types hard to read.
 
 If you are looking for a quick and dirty way of introducing a new type
 together with its properties: declare the type and state its properties as
@@ -54,7 +52,7 @@
 However, we strongly discourage this approach, except at explorative stages
 of your development. It is extremely easy to write down contradictory sets of
 axioms, in which case you will be able to prove everything but it will mean
-nothing.  Here the axiomatic approach is
+nothing.  In the example above, the axiomatic approach is
 unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
 \end{isamarkuptext}%
 %
@@ -70,7 +68,7 @@
 a type definition is merely a notational device: you introduce a new name for
 a subset of an existing type. This does not add any logical power to HOL,
 because you could base all your work directly on the subset of the existing
-type. However, the resulting theories could easily become undigestible
+type. However, the resulting theories could easily become indigestible
 because instead of implicit types you would have explicit sets in your
 formulae.
 
@@ -91,7 +89,7 @@
 \isacommand{by}\ simp%
 \begin{isamarkuptext}%
 This type definition introduces the new type \isa{three} and asserts
-that it is a \emph{copy} of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
+that it is a copy of the set \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. This assertion
 is expressed via a bijection between the \emph{type} \isa{three} and the
 \emph{set} \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}. To this end, the command declares the following
 constants behind the scenes:
@@ -102,7 +100,7 @@
 \isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
 \end{tabular}
 \end{center}
-Constant \isa{three} is explicitly defined as the representing set:
+where constant \isa{three} is explicitly defined as the representing set:
 \begin{center}
 \isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
 \end{center}
@@ -230,7 +228,7 @@
 \noindent
 This substitution step worked nicely because there was just a single
 occurrence of a term of type \isa{three}, namely \isa{x}.
-When we now apply the lemma, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:%
+When we now apply \isa{cases{\isacharunderscore}lemma}, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}%
 \begin{isamarkuptxt}%
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Types/types.tex
--- a/doc-src/TutorialI/Types/types.tex	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/types.tex	Wed Mar 07 15:54:11 2001 +0100
@@ -43,11 +43,11 @@
 Isabelle offers the related concept of an \textbf{axiomatic type class}.
 Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\ 
 an axiomatic specification of a class of types. Thus we can talk about a type
-$t$ being in a class $c$, which is written $\tau :: c$.  This is the case if
-$\tau$ satisfies the axioms of $c$. Furthermore, type classes can be
-organized in a hierarchy. Thus there is the notion of a class $d$ being a
-\textbf{subclass} of a class $c$, written $d < c$. This is the case if all
-axioms of $c$ are also provable in $d$. Let us now introduce these concepts
+$t$ being in a class $C$, which is written $\tau :: C$.  This is the case if
+$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
+organized in a hierarchy. Thus there is the notion of a class $D$ being a
+\textbf{subclass} of a class $C$, written $D < C$. This is the case if all
+axioms of $C$ are also provable in $D$. We introduce these concepts
 by means of a running example, ordering relations.
 
 \subsection{Overloading}
diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Mar 07 15:54:11 2001 +0100
@@ -62,6 +62,8 @@
 I guess we should say "HOL" everywhere, with a remark early on about the
 differences between our HOL and the other one.
 
+Syntax translations! Harpoons already used!
+
 warning: simp of asms from l to r; may require reordering (rotate_tac)
 
 Adjust FP textbook refs: new Bird, Hudak