doc-src/TutorialI/Misc/arith3.thy
changeset 8745 13b32661dde4
equal deleted inserted replaced
8744:22fa8b16c3ae 8745:13b32661dde4
       
     1 (*<*)
       
     2 theory arith3 = Main:;
       
     3 (*>*)
       
     4 lemma "n*n = n \\<Longrightarrow> n=0 \\<or> n=1";
       
     5 (**)(*<*)
       
     6 oops;
       
     7 end
       
     8 (*>*)