src/HOL/Word/WordDefinition.thy

 
 (* We do sint before sbin, before sint is the user version
    and interpretations do not produce thm duplicates. I.e. 
    we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
    because the latter is the same thm as the former *)
-interpretation word_sint:
-  td_ext ["sint ::'a::len word => int" 
+interpretation word_sint!:
+  td_ext "sint ::'a::len word => int" 
           word_of_int 
           "sints (len_of TYPE('a::len))"
           "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
-               2 ^ (len_of TYPE('a::len) - 1)"]
+               2 ^ (len_of TYPE('a::len) - 1)"
   by (rule td_ext_sint)
 
-interpretation word_sbin:
-  td_ext ["sint ::'a::len word => int" 
+interpretation word_sbin!:
+  td_ext "sint ::'a::len word => int" 
           word_of_int 
           "sints (len_of TYPE('a::len))"
-          "sbintrunc (len_of TYPE('a::len) - 1)"]
+          "sbintrunc (len_of TYPE('a::len) - 1)"
   by (rule td_ext_sbin)
 
 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard]
 
 lemmas td_sint = word_sint.td

   apply safe
   apply (drule sym)
   apply simp
   done
 
-interpretation word_bl:
-  type_definition ["to_bl :: 'a::len0 word => bool list"
-                   of_bl  
-                   "{bl. length bl = len_of TYPE('a::len0)}"]
+interpretation word_bl!:
+  type_definition "to_bl :: 'a::len0 word => bool list"
+                  of_bl  
+                  "{bl. length bl = len_of TYPE('a::len0)}"
   by (rule td_bl)
 
 lemma word_size_bl: "size w == size (to_bl w)"
   unfolding word_size by auto