doc-src/TutorialI/Types/Typedef.thy
changeset 10654 458068404143
parent 10420 ef006735bee8
child 10885 90695f46440b
     1.1 --- a/doc-src/TutorialI/Types/Typedef.thy	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Types/Typedef.thy	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4  @{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
     1.5  representation: *}
     1.6  
     1.7 -lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow>  Q(n::nat)";
     1.8 +lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n : three \<rbrakk> \<Longrightarrow>  Q n";
     1.9  
    1.10  txt{*\noindent
    1.11  Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated