src/HOL/HOL.thy
changeset 31998 2c7a24f74db9
parent 31956 c3844c4d0c2c
child 32068 98acc234d683
     1.1 --- a/src/HOL/HOL.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -1787,7 +1787,7 @@
     1.4    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
     1.5  begin
     1.6  
     1.7 -lemma eq [code unfold, code inline del]: "eq = (op =)"
     1.8 +lemma eq [code_unfold, code_inline del]: "eq = (op =)"
     1.9    by (rule ext eq_equals)+
    1.10  
    1.11  lemma eq_refl: "eq x x \<longleftrightarrow> True"
    1.12 @@ -1796,7 +1796,7 @@
    1.13  lemma equals_eq: "(op =) \<equiv> eq"
    1.14    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    1.15  
    1.16 -declare equals_eq [symmetric, code post]
    1.17 +declare equals_eq [symmetric, code_post]
    1.18  
    1.19  end
    1.20  
    1.21 @@ -1847,7 +1847,7 @@
    1.22  
    1.23  lemmas [code] = Let_def if_True if_False
    1.24  
    1.25 -lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
    1.26 +lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
    1.27  
    1.28  instantiation itself :: (type) eq
    1.29  begin