equal
deleted
inserted
replaced
276 instance int :: linorder |
276 instance int :: linorder |
277 by intro_classes (rule zle_linear) |
277 by intro_classes (rule zle_linear) |
278 |
278 |
279 |
279 |
280 lemmas zless_linear = linorder_less_linear [where 'a = int] |
280 lemmas zless_linear = linorder_less_linear [where 'a = int] |
|
281 lemmas linorder_neqE_int = linorder_neqE[where 'a = int] |
281 |
282 |
282 |
283 |
283 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" |
284 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" |
284 by (simp add: Zero_int_def) |
285 by (simp add: Zero_int_def) |
285 |
286 |