changeset 10171 | 59d6633835fa |
parent 9458 | c613cd06d5cf |
10170:dfff821d2949 | 10171:59d6633835fa |
---|---|
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 by(auto); |
6 by(auto); |
7 end |
7 end |
8 (*>*) |
8 (*>*) |