--- a/src/HOL/HOL.thy Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/HOL.thy Thu Sep 25 09:28:03 2008 +0200
@@ -1710,16 +1710,24 @@
class eq = type +
fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
- assumes eq: "eq x y \<longleftrightarrow> x = y "
+ assumes eq_equals: "eq x y \<longleftrightarrow> x = y "
begin
+lemma eq: "eq = (op =)"
+ by (rule ext eq_equals)+
+
lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
- by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
+ by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
declare equals_eq [symmetric, code post]
+lemma eq_refl: "eq x x \<longleftrightarrow> True"
+ unfolding eq by rule+
+
end
+declare simp_thms(6) [code nbe]
+
hide (open) const eq
hide const eq