| changeset 9458 | c613cd06d5cf |
| parent 8745 | 13b32661dde4 |
| child 10171 | 59d6633835fa |
| 9457:966974a7a5b3 | 9458:c613cd06d5cf |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory arith1 = Main:; |
2 theory arith1 = Main:; |
3 (*>*) |
3 (*>*) |
4 lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n"; |
4 lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n"; |
5 (**)(*<*) |
5 (**)(*<*) |
6 apply(auto).; |
6 by(auto); |
7 end |
7 end |
8 (*>*) |
8 (*>*) |