changeset 36635 | 080b755377c0 |
parent 32149 | ef59550a55d3 |
child 37117 | 59cee8807c29 |
--- a/src/HOL/Word/WordArith.thy Tue May 04 08:55:39 2010 +0200 +++ b/src/HOL/Word/WordArith.thy Tue May 04 08:55:43 2010 +0200 @@ -17,7 +17,7 @@ by (auto simp del: word_uint.Rep_inject simp: word_uint.Rep_inject [symmetric]) -lemma signed_linorder: "linorder word_sle word_sless" +lemma signed_linorder: "class.linorder word_sle word_sless" proof qed (unfold word_sle_def word_sless_def, auto)