src/HOL/HOL.thy
changeset 30966 55104c664185
parent 30947 dd551284a300
child 30970 3fe2e418a071
     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 *}