equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 \begin{isabelle}% |
2 \isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline |
2 \isacommand{lemma}\ {\isachardoublequote}min\ i\ {\isacharparenleft}max\ j\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ max\ {\isacharparenleft}min\ {\isacharparenleft}k{\isacharasterisk}k{\isacharparenright}\ i{\isacharparenright}\ {\isacharparenleft}min\ i\ {\isacharparenleft}j{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline |
3 \isacommand{by}(arith)\isanewline |
3 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline |
4 \end{isabelle}% |
4 \end{isabelle}% |
5 %%% Local Variables: |
5 %%% Local Variables: |
6 %%% mode: latex |
6 %%% mode: latex |
7 %%% TeX-master: "root" |
7 %%% TeX-master: "root" |
8 %%% End: |
8 %%% End: |