--- a/src/HOL/HOL.thy Wed Apr 22 19:16:02 2009 +0200
+++ b/src/HOL/HOL.thy Thu Apr 23 12:17:50 2009 +0200
@@ -1737,13 +1737,16 @@
lemma eq_refl: "eq x x \<longleftrightarrow> True"
unfolding eq by rule+
-lemma equals_eq [code inline, code]: "(op =) \<equiv> eq"
+lemma equals_eq [code inline]: "(op =) \<equiv> eq"
by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
declare equals_eq [symmetric, code post]
end
+declare equals_eq [code]
+
+
subsubsection {* Generic code generator foundation *}
text {* Datatypes *}
--- 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.*}