author | nipkow |
Tue, 31 Oct 2000 08:53:12 +0100 | |
changeset 10362 | c6b197ccf1f1 |
parent 10267 | 325ead6d9457 |
permissions | -rw-r--r-- |
% \begin{isabellebody}% \def\isabellecontext{arith{\isadigit{1}}}% \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" %%% End: