| changeset 9541 | d17c0b34d5c8 |
| parent 9145 | 9f7b8de5bfaf |
| child 9673 | 1b2d4f995b13 |
| 9540:02c51ca9c531 | 9541:d17c0b34d5c8 |
|---|---|
1 \begin{isabelle}% |
1 \begin{isabelle}% |
2 \isacommand{lemma}~{"}{\isasymnot}~m~<~n~{\isasymand}~m~<~n+1~{\isasymLongrightarrow}~m~=~n{"}\isanewline |
2 \isacommand{lemma}\ {"}{\isasymnot}\ m\ <\ n\ {\isasymand}\ m\ <\ n+1\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline |
3 \end{isabelle}% |
3 \end{isabelle}% |
4 %%% Local Variables: |
4 %%% Local Variables: |
5 %%% mode: latex |
5 %%% mode: latex |
6 %%% TeX-master: "root" |
6 %%% TeX-master: "root" |
7 %%% End: |
7 %%% End: |