equal
deleted
inserted
replaced
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{arith{\isadigit{2}}}% |
|
4 \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 |
|
5 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
6 \end{isabellebody}% |
|
7 %%% Local Variables: |
|
8 %%% mode: latex |
|
9 %%% TeX-master: "root" |
|
10 %%% End: |
|