src/HOL/Word/Word.thy
changeset 46026 83caa4f4bd56
parent 46025 64a19ea435fc
child 46057 8664713db181
     1.1 --- a/src/HOL/Word/Word.thy	Wed Dec 28 22:08:44 2011 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Dec 29 10:47:54 2011 +0100
     1.3 @@ -507,10 +507,12 @@
     1.4  
     1.5  lemmas td_sint = word_sint.td
     1.6  
     1.7 -lemma word_number_of_alt [code_unfold_post]:
     1.8 +lemma word_number_of_alt:
     1.9    "number_of b = word_of_int (number_of b)"
    1.10    by (simp add: number_of_eq word_number_of_def)
    1.11  
    1.12 +declare word_number_of_alt [symmetric, code_abbrev]
    1.13 +
    1.14  lemma word_no_wi: "number_of = word_of_int"
    1.15    by (auto simp: word_number_of_def)
    1.16