src/HOL/Nat_Numeral.thy
changeset 31998 2c7a24f74db9
parent 31790 05c92381363c
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/Nat_Numeral.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -20,13 +20,13 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
     1.8 +  nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
     1.9  
    1.10  instance ..
    1.11  
    1.12  end
    1.13  
    1.14 -lemma [code post]:
    1.15 +lemma [code_post]:
    1.16    "nat (number_of v) = number_of v"
    1.17    unfolding nat_number_of_def ..
    1.18  
    1.19 @@ -316,13 +316,13 @@
    1.20  lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
    1.21  by (simp add: nat_number_of_def)
    1.22  
    1.23 -lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
    1.24 +lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
    1.25  by (simp add: nat_number_of_def)
    1.26  
    1.27  lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
    1.28  by (simp add: nat_1 nat_number_of_def)
    1.29  
    1.30 -lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
    1.31 +lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
    1.32  by (simp add: nat_numeral_1_eq_1)
    1.33  
    1.34