| author | nipkow |
| Mon, 09 Oct 2000 10:18:21 +0200 | |
| changeset 10171 | 59d6633835fa |
| parent 9458 | c613cd06d5cf |
| permissions | -rw-r--r-- |
| nipkow@8745 | 1 |
(*<*) |
| nipkow@8745 | 2 |
theory arith1 = Main:; |
| nipkow@8745 | 3 |
(*>*) |
| nipkow@10171 | 4 |
lemma "\<lbrakk> \<not> m < n; m < n+1 \<rbrakk> \<Longrightarrow> m = n"; |
| nipkow@8745 | 5 |
(**)(*<*) |
| nipkow@9458 | 6 |
by(auto); |
| nipkow@8745 | 7 |
end |
| nipkow@8745 | 8 |
(*>*) |