\begin{isabelle}% \isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline \isacommand{by}(arith)\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" %%% End: