doc-src/TutorialI/Misc/arith1.thy
changeset 10171 59d6633835fa
parent 9458 c613cd06d5cf
equal deleted inserted replaced
10170:dfff821d2949 10171:59d6633835fa
     1 (*<*)
     1 (*<*)
     2 theory arith1 = Main:;
     2 theory arith1 = Main:;
     3 (*>*)
     3 (*>*)
     4 lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n";
     4 lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n";
     5 (**)(*<*)
     5 (**)(*<*)
     6 by(auto);
     6 by(auto);
     7 end
     7 end
     8 (*>*)
     8 (*>*)