| changeset 19044 | d4bc0ee9383a |
| parent 18915 | 7521b849ae98 |
| child 19138 | 42ff710d432f |
--- a/src/HOL/Integ/IntDef.thy Wed Feb 15 18:10:09 2006 +0100 +++ b/src/HOL/Integ/IntDef.thy Wed Feb 15 19:01:09 2006 +0100 @@ -281,7 +281,6 @@ lemmas zless_linear = linorder_less_linear [where 'a = int] -lemmas linorder_neqE_int = linorder_neqE[where 'a = int] lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"