src/HOL/Nat.thy
changeset 31998 2c7a24f74db9
parent 31714 347e9d18f372
child 32437 66f1a0dfe7d9
     1.1 --- a/src/HOL/Nat.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -1200,9 +1200,9 @@
     1.4  text {* for code generation *}
     1.5  
     1.6  definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
     1.7 -  funpow_code_def [code post]: "funpow = compow"
     1.8 +  funpow_code_def [code_post]: "funpow = compow"
     1.9  
    1.10 -lemmas [code unfold] = funpow_code_def [symmetric]
    1.11 +lemmas [code_unfold] = funpow_code_def [symmetric]
    1.12  
    1.13  lemma [code]:
    1.14    "funpow 0 f = id"
    1.15 @@ -1265,7 +1265,7 @@
    1.16  
    1.17  end
    1.18  
    1.19 -declare of_nat_code [code, code unfold, code inline del]
    1.20 +declare of_nat_code [code, code_unfold, code_inline del]
    1.21  
    1.22  text{*Class for unital semirings with characteristic zero.
    1.23   Includes non-ordered rings like the complex numbers.*}