--- a/src/HOL/Word/WordArith.thy Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Thu Mar 26 20:08:55 2009 +0100
@@ -21,7 +21,7 @@
proof
qed (unfold word_sle_def word_sless_def, auto)
-interpretation signed!: linorder "word_sle" "word_sless"
+interpretation signed: linorder "word_sle" "word_sless"
by (rule signed_linorder)
lemmas word_arith_wis =
@@ -862,7 +862,7 @@
lemmas td_ext_unat = refl [THEN td_ext_unat']
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
-interpretation word_unat!:
+interpretation word_unat:
td_ext "unat::'a::len word => nat"
of_nat
"unats (len_of TYPE('a::len))"