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