--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Sun Dec 29 18:31:31 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Sun Dec 29 23:12:39 2002 +0100
@@ -48,7 +48,7 @@
The same game can be played with other datatypes, for example lists,
where @{term tl} is the tail of a list, and @{text length} returns a
natural number:
-\Tweakskip
+%\Tweakskip
*}
(*<*)declare length_tl[simp del](*>*)
lemma "length(tl xs) = length xs - 1"
@@ -286,7 +286,8 @@
equation.
The proof is so simple that it can be condensed to
-\Tweakskip*}
+%\Tweakskip
+*}
(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
by (induct xs rule: rot.induct, simp_all)