| changeset 29509 | 1ff0f3f08a7b |
| parent 29235 | 2d62b637fa80 |
| child 29631 | 3aa049e5f156 |
| child 29667 | 53103fc8ffa3 |
--- a/src/HOL/Word/WordArith.thy Fri Jan 16 08:29:11 2009 +0100 +++ b/src/HOL/Word/WordArith.thy Fri Jan 16 14:58:11 2009 +0100 @@ -22,7 +22,7 @@ proof qed (unfold word_sle_def word_sless_def, auto) -class_interpretation signed: linorder ["word_sle" "word_sless"] +interpretation signed!: linorder "word_sle" "word_sless" by (rule signed_linorder) lemmas word_arith_wis =