doc-src/TutorialI/Misc/arith4.thy
author nipkow
Mon, 28 Aug 2000 09:32:51 +0200
changeset 9689 751fde5307e4
parent 9458 c613cd06d5cf
permissions -rw-r--r--
*** empty log message ***

(*<*)
theory arith4 = Main:;
(*>*)
lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
(**)(*<*)
by(arith);
end
(*>*)