--- a/doc-src/TutorialI/Misc/Itrev.thy Mon Oct 30 18:28:00 2000 +0100
+++ b/doc-src/TutorialI/Misc/Itrev.thy Tue Oct 31 08:53:12 2000 +0100
@@ -35,7 +35,7 @@
gradually, using only @{text"#"}:
*}
-consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
+consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list";
primrec
"itrev [] ys = ys"
"itrev (x#xs) ys = itrev xs (x#ys)";
@@ -75,7 +75,7 @@
*};
(*<*)oops;(*>*)
lemma "itrev xs ys = rev xs @ ys";
-
+(*<*)apply(induct_tac xs, simp_all)(*>*)
txt{*\noindent
If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
@{term"rev xs"}, just as required.
@@ -87,11 +87,7 @@
Although we now have two variables, only @{term"xs"} is suitable for
induction, and we repeat our above proof attempt. Unfortunately, we are still
not there:
-\begin{isabelle}\makeatother
-~1.~{\isasymAnd}a~list.\isanewline
-~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
-\end{isabelle}
+@{subgoals[display,indent=0,goals_limit=1]}
The induction hypothesis is still too weak, but this time it takes no
intuition to generalize: the problem is that @{term"ys"} is fixed throughout
the subgoal, but the induction hypothesis needs to be applied with
@@ -99,7 +95,7 @@
for all @{term"ys"} instead of a fixed one:
*};
(*<*)oops;(*>*)
-lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
+lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
(*<*)
by(induct_tac xs, simp_all);
(*>*)