doc-src/TutorialI/Misc/arith2.thy
author wenzelm
Fri, 15 Sep 2000 19:07:55 +0200
changeset 9989 3788cb659e0c
parent 9458 c613cd06d5cf
child 10171 59d6633835fa
permissions -rw-r--r--
tentative fix while hunting gremlins ...;

(*<*)
theory arith2 = Main:;
(*>*)
lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
by(arith);
(**)(*<*)
end
(*>*)