author | nipkow |
Fri, 03 Nov 2000 17:14:06 +0100 | |
changeset 10373 | f9211fc8cd7d |
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: