--- a/doc-src/TutorialI/Types/Typedef.thy Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/Types/Typedef.thy Wed Dec 13 09:39:53 2000 +0100
@@ -199,7 +199,7 @@
@{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
representation: *}
-lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow> Q(n::nat)";
+lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow> Q n";
txt{*\noindent
Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated