src/HOL/Nat.thy
changeset 30966 55104c664185
parent 30954 cf50e67bc1d1
child 30971 7fbebf75b3ef
     1.1 --- a/src/HOL/Nat.thy	Wed Apr 22 19:16:02 2009 +0200
     1.2 +++ b/src/HOL/Nat.thy	Thu Apr 23 12:17:50 2009 +0200
     1.3 @@ -1220,7 +1220,7 @@
     1.4    "of_nat_aux inc 0 i = i"
     1.5    | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
     1.6  
     1.7 -lemma of_nat_code [code, code unfold, code inline del]:
     1.8 +lemma of_nat_code:
     1.9    "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
    1.10  proof (induct n)
    1.11    case 0 then show ?case by simp
    1.12 @@ -1232,9 +1232,11 @@
    1.13      by simp
    1.14    with Suc show ?case by (simp add: add_commute)
    1.15  qed
    1.16 -    
    1.17 +
    1.18  end
    1.19  
    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.*}
    1.24