doc-src/TutorialI/Misc/arith2.thy

renamed // to / (which is what we want anyway) to avoid clash with the new
use of // for quotienting

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