src/HOL/Int.thy
changeset 32069 6d28bbd33e2c
parent 31998 2c7a24f74db9
child 32272 cc1bf9077167
     1.1 --- a/src/HOL/Int.thy	Tue Jul 14 16:27:31 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Tue Jul 14 16:27:32 2009 +0200
     1.3 @@ -2126,11 +2126,11 @@
     1.4  
     1.5  hide (open) const nat_aux
     1.6  
     1.7 -lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
     1.8 +lemma zero_is_num_zero [code, code_unfold_post]:
     1.9    "(0\<Colon>int) = Numeral0" 
    1.10    by simp
    1.11  
    1.12 -lemma one_is_num_one [code, code_inline, symmetric, code_post]:
    1.13 +lemma one_is_num_one [code, code_unfold_post]:
    1.14    "(1\<Colon>int) = Numeral1" 
    1.15    by simp
    1.16