--- a/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Mon Dec 30 18:33:15 2002 +0100
+++ b/doc-src/TutorialI/IsarOverview/Isar/Induction.thy Fri Jan 03 10:24:24 2003 +0100
@@ -8,7 +8,7 @@
and @{text Cons}. @{text Nil} is written @{term"[]"} and @{text"Cons x
xs"} is written @{term"x # xs"}. *}
-subsection{*Case distinction*}
+subsection{*Case distinction\label{sec:CaseDistinction}*}
text{* We have already met the @{text cases} method for performing
binary case splits. Here is another example: *}
@@ -47,7 +47,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:
+natural number (remember: $0-1=0$):
%\Tweakskip
*}
(*<*)declare length_tl[simp del](*>*)
@@ -286,7 +286,7 @@
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)