src/HOL/Int.thy
changeset 31998 2c7a24f74db9
parent 31100 6a2e67fe4488
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/Int.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -650,11 +650,11 @@
     1.4  
     1.5  text {* Removal of leading zeroes *}
     1.6  
     1.7 -lemma Bit0_Pls [simp, code post]:
     1.8 +lemma Bit0_Pls [simp, code_post]:
     1.9    "Bit0 Pls = Pls"
    1.10    unfolding numeral_simps by simp
    1.11  
    1.12 -lemma Bit1_Min [simp, code post]:
    1.13 +lemma Bit1_Min [simp, code_post]:
    1.14    "Bit1 Min = Min"
    1.15    unfolding numeral_simps by simp
    1.16  
    1.17 @@ -2126,11 +2126,11 @@
    1.18  
    1.19  hide (open) const nat_aux
    1.20  
    1.21 -lemma zero_is_num_zero [code, code inline, symmetric, code post]:
    1.22 +lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
    1.23    "(0\<Colon>int) = Numeral0" 
    1.24    by simp
    1.25  
    1.26 -lemma one_is_num_one [code, code inline, symmetric, code post]:
    1.27 +lemma one_is_num_one [code, code_inline, symmetric, code_post]:
    1.28    "(1\<Colon>int) = Numeral1" 
    1.29    by simp
    1.30