equal
deleted
inserted
replaced
216 by linarith |
216 by linarith |
217 |
217 |
218 lemma "(0::int) < 1" |
218 lemma "(0::int) < 1" |
219 by linarith |
219 by linarith |
220 |
220 |
221 lemma "(47::nat) + 11 < 08 * 15" |
221 lemma "(47::nat) + 11 < 8 * 15" |
222 by linarith |
222 by linarith |
223 |
223 |
224 lemma "(47::int) + 11 < 08 * 15" |
224 lemma "(47::int) + 11 < 8 * 15" |
225 by linarith |
225 by linarith |
226 |
226 |
227 text {* Splitting of inequalities of different type. *} |
227 text {* Splitting of inequalities of different type. *} |
228 |
228 |
229 lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==> |
229 lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==> |