1 (*<*)
2 theory arith2 = Main:;
3 (*>*)
4 lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
5 apply(arith);
6 (**)(*<*)
7 done
8 end
9 (*>*)