--- a/src/HOL/Nat.thy Wed Apr 22 19:16:02 2009 +0200
+++ b/src/HOL/Nat.thy Thu Apr 23 12:17:50 2009 +0200
@@ -1220,7 +1220,7 @@
"of_nat_aux inc 0 i = i"
| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *}
-lemma of_nat_code [code, code unfold, code inline del]:
+lemma of_nat_code:
"of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0"
proof (induct n)
case 0 then show ?case by simp
@@ -1232,9 +1232,11 @@
by simp
with Suc show ?case by (simp add: add_commute)
qed
-
+
end
+declare of_nat_code [code, code unfold, code inline del]
+
text{*Class for unital semirings with characteristic zero.
Includes non-ordered rings like the complex numbers.*}