1.1 --- a/src/HOL/HOL.thy Wed Apr 22 19:16:02 2009 +0200
1.2 +++ b/src/HOL/HOL.thy Thu Apr 23 12:17:50 2009 +0200
1.3 @@ -1737,13 +1737,16 @@
1.4 lemma eq_refl: "eq x x \<longleftrightarrow> True"
1.5 unfolding eq by rule+
1.6
1.7 -lemma equals_eq [code inline, code]: "(op =) \<equiv> eq"
1.8 +lemma equals_eq [code inline]: "(op =) \<equiv> eq"
1.9 by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
1.10
1.11 declare equals_eq [symmetric, code post]
1.12
1.13 end
1.14
1.15 +declare equals_eq [code]
1.16 +
1.17 +
1.18 subsubsection {* Generic code generator foundation *}
1.19
1.20 text {* Datatypes *}