src/HOL/Code_Numeral.thy
changeset 31998 2c7a24f74db9
parent 31377 a48f9ef9de15
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -176,16 +176,16 @@
     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_inline, code]:
     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 +lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
    1.13    using zero_code_numeral_code ..
    1.14  
    1.15 -lemma one_code_numeral_code [code inline, code]:
    1.16 +lemma one_code_numeral_code [code_inline, code]:
    1.17    "(1\<Colon>code_numeral) = Numeral1"
    1.18    by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
    1.19 -lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
    1.20 +lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
    1.21    using one_code_numeral_code ..
    1.22  
    1.23  lemma plus_code_numeral_code [code nbe]: