doc-src/TutorialI/Misc/document/arith2.tex

do nat pass theory value, but sg_ref;

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