src/HOL/HOL.thy
changeset 28346 b8390cd56b8f
parent 28325 0b6b83ec8458
child 28400 89904cfd41c3
     1.1 --- a/src/HOL/HOL.thy	Wed Sep 24 19:39:25 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Sep 25 09:28:03 2008 +0200
     1.3 @@ -1710,16 +1710,24 @@
     1.4  
     1.5  class eq = type +
     1.6    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.7 -  assumes eq: "eq x y \<longleftrightarrow> x = y "
     1.8 +  assumes eq_equals: "eq x y \<longleftrightarrow> x = y "
     1.9  begin
    1.10  
    1.11 +lemma eq: "eq = (op =)"
    1.12 +  by (rule ext eq_equals)+
    1.13 +
    1.14  lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
    1.15 -  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
    1.16 +  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    1.17  
    1.18  declare equals_eq [symmetric, code post]
    1.19  
    1.20 +lemma eq_refl: "eq x x \<longleftrightarrow> True"
    1.21 +  unfolding eq by rule+
    1.22 +
    1.23  end
    1.24  
    1.25 +declare simp_thms(6) [code nbe]
    1.26 +
    1.27  hide (open) const eq
    1.28  hide const eq
    1.29