diff -r 2626d4e37341 -r 9554ce1c2e54 doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Oct 19 21:25:15 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Fri Oct 20 08:46:41 2000 +0200
@@ -6,7 +6,8 @@
 Now that we have learned about rules and logic, we take another look at the
 finer points of induction. The two questions we answer are: what to do if the
 proposition to be proved is not directly amenable to induction, and how to
-utilize and even derive new induction schemas.
+utilize and even derive new induction schemas. We conclude with some slightly subtle
+examples of induction.
 *};
 
 subsection{*Massaging the proposition*};
@@ -82,7 +83,7 @@
 Here is a simple example (which is proved by @{text"blast"}):
 *};
 
-lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
 (*<*)by blast;(*>*)
 
 text{*\noindent
@@ -105,7 +106,7 @@
 statement of your original lemma, thus avoiding the intermediate step:
 *};
 
-lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
+lemma myrule[rule_format]:  "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
 (*<*)
 by blast;
 (*>*)
@@ -129,6 +130,9 @@
 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
 For an example see \S\ref{sec:CTL-revisited} below.
+
+Of course, all premises that share free variables with $t$ need to be pulled into
+the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
 *};
 
 subsection{*Beyond structural and recursion induction*};
@@ -149,7 +153,7 @@
 Here is an example of its application.
 *};
 
-consts f :: "nat => nat";
+consts f :: "nat \<Rightarrow> nat";
 axioms f_ax: "f(f(n)) < f(Suc(n))";
 
 text{*\noindent
@@ -289,7 +293,6 @@
 by(insert induct_lem, blast);
 
 text{*
-
 Finally we should mention that HOL already provides the mother of all
 inductions, \textbf{well-founded
 induction}\indexbold{induction!well-founded}\index{well-founded