src/HOL/Code_Numeral.thy
changeset 32069 6d28bbd33e2c
parent 31998 2c7a24f74db9
child 33296 a3924d1069e5
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Jul 14 16:27:31 2009 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 16:27:32 2009 +0200
     1.3 @@ -176,13 +176,13 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma zero_code_numeral_code [code_inline, code]:
     1.8 +lemma zero_code_numeral_code [code, code_unfold]:
     1.9    "(0\<Colon>code_numeral) = Numeral0"
    1.10    by (simp add: number_of_code_numeral_def Pls_def)
    1.11  lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
    1.12    using zero_code_numeral_code ..
    1.13  
    1.14 -lemma one_code_numeral_code [code_inline, code]:
    1.15 +lemma one_code_numeral_code [code, code_unfold]:
    1.16    "(1\<Colon>code_numeral) = Numeral1"
    1.17    by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
    1.18  lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"