# HG changeset patch
# User haftmann
# Date 1282930463 -7200
# Node ID 97775f3e8722748553a668a9bad709a1e7c23e92
# Parent  168dba35ecf327410aca2c94562e019ffdc8b5ec
renamed class/constant eq to equal; tuned some instantiations

diff -r 168dba35ecf3 -r 97775f3e8722 NEWS
--- a/NEWS	Fri Aug 27 15:36:02 2010 +0200
+++ b/NEWS	Fri Aug 27 19:34:23 2010 +0200
@@ -56,6 +56,10 @@
 
 *** HOL ***
 
+* Renamed class eq and constant eq (for code generation) to class equal
+and constant equal, plus renaming of related facts and various tuning.
+INCOMPATIBILITY.
+
 * Scala (2.8 or higher) has been added to the target languages of
 the code generator.
 
diff -r 168dba35ecf3 -r 97775f3e8722 doc-src/Codegen/Thy/Foundations.thy
--- a/doc-src/Codegen/Thy/Foundations.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -220,12 +220,12 @@
 text {*
   \noindent Obviously, polymorphic equality is implemented the Haskell
   way using a type class.  How is this achieved?  HOL introduces an
-  explicit class @{class eq} with a corresponding operation @{const
-  eq_class.eq} such that @{thm eq [no_vars]}.  The preprocessing
-  framework does the rest by propagating the @{class eq} constraints
+  explicit class @{class equal} with a corresponding operation @{const
+  HOL.equal} such that @{thm equal [no_vars]}.  The preprocessing
+  framework does the rest by propagating the @{class equal} constraints
   through all dependent code equations.  For datatypes, instances of
-  @{class eq} are implicitly derived when possible.  For other types,
-  you may instantiate @{text eq} manually like any other type class.
+  @{class equal} are implicitly derived when possible.  For other types,
+  you may instantiate @{text equal} manually like any other type class.
 *}
 
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -162,7 +162,7 @@
 subsubsection {* Code generator setup *}
 
 lemmas [code del] = term.recs term.cases term.size
-lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
+lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
 
 lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
 lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -115,12 +115,12 @@
 lemmas [code del] = code_numeral.recs code_numeral.cases
 
 lemma [code]:
-  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
-  by (cases k, cases l) (simp add: eq)
+  "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
+  by (cases k, cases l) (simp add: equal)
 
 lemma [code nbe]:
-  "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
-  by (rule HOL.eq_refl)
+  "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
+  by (rule equal_refl)
 
 
 subsection {* Code numerals as datatype of ints *}
@@ -301,7 +301,7 @@
   (Haskell "Integer")
   (Scala "BigInt")
 
-code_instance code_numeral :: eq
+code_instance code_numeral :: equal
   (Haskell -)
 
 setup {*
@@ -342,7 +342,7 @@
   (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
 
-code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/HOL.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -1775,31 +1775,30 @@
 
 subsubsection {* Equality *}
 
-class eq =
-  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
+class equal =
+  fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
 begin
 
-lemma eq [code_unfold, code_inline del]: "eq = (op =)"
-  by (rule ext eq_equals)+
+lemma equal [code_unfold, code_inline del]: "equal = (op =)"
+  by (rule ext equal_eq)+
 
-lemma eq_refl: "eq x x \<longleftrightarrow> True"
-  unfolding eq by rule+
+lemma equal_refl: "equal x x \<longleftrightarrow> True"
+  unfolding equal by rule+
 
-lemma equals_eq: "(op =) \<equiv> eq"
-  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
-
-declare equals_eq [symmetric, code_post]
+lemma eq_equal: "(op =) \<equiv> equal"
+  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
 
 end
 
-declare equals_eq [code]
+declare eq_equal [symmetric, code_post]
+declare eq_equal [code]
 
 setup {*
   Code_Preproc.map_pre (fn simpset =>
-    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
+    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
       (fn thy => fn _ => fn Const (_, T) => case strip_type T
-        of (Type _ :: _, _) => SOME @{thm equals_eq}
+        of (Type _ :: _, _) => SOME @{thm eq_equal}
          | _ => NONE)])
 *}
 
@@ -1839,50 +1838,50 @@
     and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
     and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
 
-instantiation itself :: (type) eq
+instantiation itself :: (type) equal
 begin
 
-definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
-  "eq_itself x y \<longleftrightarrow> x = y"
+definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
+  "equal_itself x y \<longleftrightarrow> x = y"
 
 instance proof
-qed (fact eq_itself_def)
+qed (fact equal_itself_def)
 
 end
 
-lemma eq_itself_code [code]:
-  "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
-  by (simp add: eq)
+lemma equal_itself_code [code]:
+  "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
+  by (simp add: equal)
 
 text {* Equality *}
 
 declare simp_thms(6) [code nbe]
 
 setup {*
-  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
+  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
 *}
 
-lemma equals_alias_cert: "OFCLASS('a, eq_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> eq)" (is "?ofclass \<equiv> ?eq")
+lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
 proof
   assume "PROP ?ofclass"
-  show "PROP ?eq"
-    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
+  show "PROP ?equal"
+    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
       (fact `PROP ?ofclass`)
 next
-  assume "PROP ?eq"
+  assume "PROP ?equal"
   show "PROP ?ofclass" proof
-  qed (simp add: `PROP ?eq`)
+  qed (simp add: `PROP ?equal`)
 qed
   
 setup {*
-  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>eq \<Rightarrow> 'a \<Rightarrow> bool"})
+  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
 *}
 
 setup {*
-  Nbe.add_const_alias @{thm equals_alias_cert}
+  Nbe.add_const_alias @{thm equal_alias_cert}
 *}
 
-hide_const (open) eq
+hide_const (open) equal
 
 text {* Cases *}
 
@@ -1939,10 +1938,10 @@
 
 text {* using built-in Haskell equality *}
 
-code_class eq
+code_class equal
   (Haskell "Eq")
 
-code_const "eq_class.eq"
+code_const "HOL.equal"
   (Haskell infixl 4 "==")
 
 code_const "op ="
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Int.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -2222,42 +2222,42 @@
   mult_bin_simps
   arith_extra_simps(4) [where 'a = int]
 
-instantiation int :: eq
+instantiation int :: equal
 begin
 
 definition
-  "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
-
-instance by default (simp add: eq_int_def)
+  "HOL.equal k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+
+instance by default (simp add: equal_int_def)
 
 end
 
 lemma eq_number_of_int_code [code]:
-  "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
-  unfolding eq_int_def number_of_is_id ..
+  "HOL.equal (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> HOL.equal k l"
+  unfolding equal_int_def number_of_is_id ..
 
 lemma eq_int_code [code]:
-  "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
-  "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
-  "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
-  "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
-  "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
-  "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
-  "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
-  "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
-  "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
-  "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
-  "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
-  "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
-  "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
-  "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
-  "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
-  "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
-  unfolding eq_equals by simp_all
+  "HOL.equal Int.Pls Int.Pls \<longleftrightarrow> True"
+  "HOL.equal Int.Pls Int.Min \<longleftrightarrow> False"
+  "HOL.equal Int.Pls (Int.Bit0 k2) \<longleftrightarrow> HOL.equal Int.Pls k2"
+  "HOL.equal Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
+  "HOL.equal Int.Min Int.Pls \<longleftrightarrow> False"
+  "HOL.equal Int.Min Int.Min \<longleftrightarrow> True"
+  "HOL.equal Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
+  "HOL.equal Int.Min (Int.Bit1 k2) \<longleftrightarrow> HOL.equal Int.Min k2"
+  "HOL.equal (Int.Bit0 k1) Int.Pls \<longleftrightarrow> HOL.equal k1 Int.Pls"
+  "HOL.equal (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
+  "HOL.equal (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
+  "HOL.equal (Int.Bit1 k1) Int.Min \<longleftrightarrow> HOL.equal k1 Int.Min"
+  "HOL.equal (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> HOL.equal k1 k2"
+  "HOL.equal (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
+  "HOL.equal (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
+  "HOL.equal (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> HOL.equal k1 k2"
+  unfolding equal_eq by simp_all
 
 lemma eq_int_refl [code nbe]:
-  "eq_class.eq (k::int) k \<longleftrightarrow> True"
-  by (rule HOL.eq_refl)
+  "HOL.equal (k::int) k \<longleftrightarrow> True"
+  by (rule equal_refl)
 
 lemma less_eq_number_of_int_code [code]:
   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Lazy_Sequence.thy
--- a/src/HOL/Lazy_Sequence.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -39,10 +39,14 @@
   "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
 by (cases xq) auto
 
-lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
-  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
-apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) 
-apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
+lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
+  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
+apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
+apply (cases yq) apply (auto simp add: equal_eq) done
+
+lemma [code nbe]:
+  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 lemma seq_case [code]:
   "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -701,7 +701,44 @@
   "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
 
-lemma [code, code del]:
-  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+lemma map_of_eqI: (*FIXME move to Map.thy*)
+  assumes set_eq: "set (map fst xs) = set (map fst ys)"
+  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
+  shows "map_of xs = map_of ys"
+proof (rule ext)
+  fix k show "map_of xs k = map_of ys k"
+  proof (cases "map_of xs k")
+    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
+    with set_eq have "k \<notin> set (map fst ys)" by simp
+    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
+    with None show ?thesis by simp
+  next
+    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
+    with map_eq show ?thesis by auto
+  qed
+qed
+
+lemma map_of_eq_dom: (*FIXME move to Map.thy*)
+  assumes "map_of xs = map_of ys"
+  shows "fst ` set xs = fst ` set ys"
+proof -
+  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
+  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
+qed
+
+lemma equal_Mapping [code]:
+  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
+    (let ks = map fst xs; ls = map fst ys
+    in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
+proof -
+  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" by (auto simp add: image_def intro!: bexI)
+  show ?thesis
+    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
+      (auto dest!: map_of_eq_dom intro: aux)
+qed
+
+lemma [code nbe]:
+  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 end
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -19,7 +19,7 @@
   #> String_Code.add_literal_list_string "Haskell"
 *}
 
-code_instance char :: eq
+code_instance char :: equal
   (Haskell -)
 
 code_reserved SML
@@ -31,7 +31,7 @@
 code_reserved Scala
   char
 
-code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) = _)")
   (OCaml "!((_ : char) = _)")
   (Haskell infixl 4 "==")
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -21,7 +21,7 @@
   (Scala "BigInt")
   (Eval "int")
 
-code_instance int :: eq
+code_instance int :: equal
   (Haskell -)
 
 setup {*
@@ -96,7 +96,7 @@
   (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
 
-code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -112,7 +112,7 @@
     false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
 *}
 
-code_instance code_numeral :: eq
+code_instance code_numeral :: equal
   (Haskell -)
 
 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
@@ -131,7 +131,7 @@
   (Haskell "divMod")
   (Scala infixl 8 "/%")
 
-code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (Haskell infixl 4 "==")
   (Scala infixl 5 "==")
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -109,16 +109,20 @@
 
 text {* Equality *}
 
-instantiation dlist :: (eq) eq
+instantiation dlist :: (equal) equal
 begin
 
-definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
+definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
 
 instance proof
-qed (simp add: eq_dlist_def eq list_of_dlist_inject)
+qed (simp add: equal_dlist_def equal list_of_dlist_inject)
 
 end
 
+lemma [code nbe]:
+  "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
+  by (fact equal_refl)
+
 
 section {* Induction principle and case distinction *}
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -55,12 +55,12 @@
   by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
 
 lemma eq_nat_code [code]:
-  "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
-  by (simp add: eq)
+  "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
+  by (simp add: equal)
 
 lemma eq_nat_refl [code nbe]:
-  "eq_class.eq (n::nat) n \<longleftrightarrow> True"
-  by (rule HOL.eq_refl)
+  "HOL.equal (n::nat) n \<longleftrightarrow> True"
+  by (rule equal_refl)
 
 lemma less_eq_nat_code [code]:
   "n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
@@ -332,7 +332,7 @@
   (Haskell "Nat.Nat")
   (Scala "Nat.Nat")
 
-code_instance nat :: eq
+code_instance nat :: equal
   (Haskell -)
 
 text {*
@@ -442,7 +442,7 @@
   (Scala infixl 8 "/%")
   (Eval "Integer.div'_mod")
 
-code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Enum.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -35,17 +35,21 @@
 
 subsection {* Equality and order on functions *}
 
-instantiation "fun" :: (enum, eq) eq
+instantiation "fun" :: (enum, equal) equal
 begin
 
 definition
-  "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
+  "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
 
 instance proof
-qed (simp_all add: eq_fun_def enum_all expand_fun_eq)
+qed (simp_all add: equal_fun_def enum_all expand_fun_eq)
 
 end
 
+lemma [code nbe]:
+  "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
+  by (fact equal_refl)
+
 lemma order_fun [code]:
   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
@@ -169,7 +173,7 @@
 
 end
 
-lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
+lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
   in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   by (simp add: enum_fun_def Let_def)
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -227,17 +227,21 @@
   "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
   by (fact less_le_not_le)
 
-instantiation fset :: (type) eq
+instantiation fset :: (type) equal
 begin
 
 definition
-  "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
+  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
 
 instance proof
-qed (simp add: eq_fset_def set_eq [symmetric])
+qed (simp add: equal_fset_def set_eq [symmetric])
 
 end
 
+lemma [code nbe]:
+  "HOL.equal (A :: 'a fset) A \<longleftrightarrow> True"
+  by (fact equal_refl)
+
 
 subsection {* Functorial operations *}
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -81,9 +81,9 @@
   by (auto simp add: prefix_def)
 
 lemma less_eq_list_code [code]:
-  "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
-  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
-  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
+  "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
+  "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
+  "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   by simp_all
 
 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/List_lexord.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -103,15 +103,15 @@
 end
 
 lemma less_list_code [code]:
-  "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
-  "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
-  "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
+  "xs < ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
+  "[] < (x\<Colon>'a\<Colon>{equal, order}) # xs \<longleftrightarrow> True"
+  "(x\<Colon>'a\<Colon>{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
   by simp_all
 
 lemma less_eq_list_code [code]:
-  "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
-  "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
-  "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
+  "x # xs \<le> ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
+  "[] \<le> (xs\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> True"
+  "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
   by simp_all
 
 end
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -280,14 +280,14 @@
 
 code_datatype empty update
 
-instantiation mapping :: (type, type) eq
+instantiation mapping :: (type, type) equal
 begin
 
 definition [code del]:
-  "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
+  "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
 
 instance proof
-qed (simp add: eq_mapping_def)
+qed (simp add: equal_mapping_def)
 
 end
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -938,17 +938,21 @@
   qed
 qed
 
-instantiation multiset :: (eq) eq
+instantiation multiset :: (equal) equal
 begin
 
 definition
-  "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
+  "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
 
 instance proof
-qed (simp add: eq_multiset_def eq_iff)
+qed (simp add: equal_multiset_def eq_iff)
 
 end
 
+lemma [code nbe]:
+  "HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True"
+  by (fact equal_refl)
+
 definition (in term_syntax)
   bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -521,22 +521,21 @@
 text {* Environments and code generation *}
 
 lemma [code, code del]:
-  fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
-  shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
+  "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
 
-lemma eq_env_code [code]:
-  fixes x y :: "'a\<Colon>eq"
-    and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
-  shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
-  eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
+lemma equal_env_code [code]:
+  fixes x y :: "'a\<Colon>equal"
+    and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
+  shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
+  HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
    of None \<Rightarrow> (case g z
         of None \<Rightarrow> True | Some _ \<Rightarrow> False)
     | Some a \<Rightarrow> (case g z
-        of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
-    and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
-    and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
-    and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
-proof (unfold eq)
+        of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
+    and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
+    and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
+    and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
+proof (unfold equal)
   have "f = g \<longleftrightarrow> (\<forall>z. case f z
    of None \<Rightarrow> (case g z
         of None \<Rightarrow> True | Some _ \<Rightarrow> False)
@@ -562,6 +561,10 @@
           of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
 qed simp_all
 
+lemma [code nbe]:
+  "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
+  by (fact equal_refl)
+
 lemma [code, code del]:
   "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -1505,23 +1505,27 @@
 
 declare pCons_0_0 [code_post]
 
-instantiation poly :: ("{zero,eq}") eq
+instantiation poly :: ("{zero, equal}") equal
 begin
 
 definition
-  "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
+  "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"
 
-instance
-  by default (rule eq_poly_def)
+instance proof
+qed (rule equal_poly_def)
 
 end
 
 lemma eq_poly_code [code]:
-  "eq_class.eq (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
-  "eq_class.eq (0::_ poly) (pCons b q) \<longleftrightarrow> eq_class.eq 0 b \<and> eq_class.eq 0 q"
-  "eq_class.eq (pCons a p) (0::_ poly) \<longleftrightarrow> eq_class.eq a 0 \<and> eq_class.eq p 0"
-  "eq_class.eq (pCons a p) (pCons b q) \<longleftrightarrow> eq_class.eq a b \<and> eq_class.eq p q"
-unfolding eq by simp_all
+  "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
+  "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q"
+  "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0"
+  "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q"
+  by (simp_all add: equal)
+
+lemma [code nbe]:
+  "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 lemmas coeff_code [code] =
   coeff_0 coeff_pCons_0 coeff_pCons_Suc
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Product_ord.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -22,8 +22,8 @@
 end
 
 lemma [code]:
-  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
-  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
+  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
+  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
   unfolding prod_le_def prod_less_def by simp_all
 
 instance prod :: (preorder, preorder) preorder proof
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/RBT.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -222,12 +222,14 @@
   "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
   by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
 
-lemma [code, code del]:
-  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+lemma equal_Mapping [code]:
+  "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
+  by (simp add: equal Mapping_def entries_lookup)
 
-lemma eq_Mapping [code]:
-  "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
-  by (simp add: eq Mapping_def entries_lookup)
+lemma [code nbe]:
+  "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
+  by (fact equal_refl)
+
 
 hide_const (open) impl_of lookup empty insert delete
   entries keys bulkload map_entry map fold
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/List.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -4721,8 +4721,8 @@
   by (simp add: null_def)
 
 lemma equal_Nil_null [code_unfold]:
-  "eq_class.eq xs [] \<longleftrightarrow> null xs"
-  by (simp add: eq eq_Nil_null)
+  "HOL.equal xs [] \<longleftrightarrow> null xs"
+  by (simp add: equal eq_Nil_null)
 
 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
   [code_post]: "maps f xs = concat (map f xs)"
@@ -4821,10 +4821,10 @@
   (Haskell "[]")
   (Scala "!Nil")
 
-code_instance list :: eq
+code_instance list :: equal
   (Haskell -)
 
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved SML
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 19:34:23 2010 +0200
@@ -202,7 +202,7 @@
   (@{const_name "top_fun_inst.top_fun"}, "'a"),
   (@{const_name "Pure.term"}, "'a"),
   (@{const_name "top_class.top"}, "'a"),
-  (@{const_name "eq_class.eq"}, "'a"),
+  (@{const_name "HOL.equal"}, "'a"),
   (@{const_name "Quotient.Quot_True"}, "'a")(*,
   (@{const_name "uminus"}, "'a"),
   (@{const_name "Nat.size"}, "'a"),
@@ -237,7 +237,7 @@
  @{const_name "top_fun_inst.top_fun"},
  @{const_name "Pure.term"},
  @{const_name "top_class.top"},
- @{const_name "eq_class.eq"},
+ @{const_name "HOL.equal"},
  @{const_name "Quotient.Quot_True"}]
 
 fun is_forbidden_mutant t =
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Option.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -99,8 +99,8 @@
   by (simp add: is_none_def)
 
 lemma [code_unfold]:
-  "eq_class.eq x None \<longleftrightarrow> is_none x"
-  by (simp add: eq is_none_none)
+  "HOL.equal x None \<longleftrightarrow> is_none x"
+  by (simp add: equal is_none_none)
 
 hide_const (open) is_none
 
@@ -116,10 +116,10 @@
   (Haskell "Nothing" and "Just")
   (Scala "!None" and "Some")
 
-code_instance option :: eq
+code_instance option :: equal
   (Haskell -)
 
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved SML
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Predicate.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -808,8 +808,12 @@
 
 lemma eq_pred_code [code]:
   fixes P Q :: "'a pred"
-  shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
-  unfolding eq by auto
+  shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
+  by (auto simp add: equal)
+
+lemma [code nbe]:
+  "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 lemma [code]:
   "pred_case f P = f (eval P)"
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Product_Type.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -21,17 +21,17 @@
   -- "prefer plain propositional version"
 
 lemma
-  shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
-    and [code]: "eq_class.eq True P \<longleftrightarrow> P" 
-    and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
-    and [code]: "eq_class.eq P True \<longleftrightarrow> P"
-    and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
-  by (simp_all add: eq)
+  shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
+    and [code]: "HOL.equal True P \<longleftrightarrow> P" 
+    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" 
+    and [code]: "HOL.equal P True \<longleftrightarrow> P"
+    and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
+  by (simp_all add: equal)
 
-code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
-code_instance bool :: eq
+code_instance bool :: equal
   (Haskell -)
 
 
@@ -92,7 +92,7 @@
 end
 
 lemma [code]:
-  "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
+  "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
 
 code_type unit
   (SML "unit")
@@ -106,10 +106,10 @@
   (Haskell "()")
   (Scala "()")
 
-code_instance unit :: eq
+code_instance unit :: equal
   (Haskell -)
 
-code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved SML
@@ -277,10 +277,10 @@
   (Haskell "!((_),/ (_))")
   (Scala "!((_),/ (_))")
 
-code_instance prod :: eq
+code_instance prod :: equal
   (Haskell -)
 
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 types_code
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Quickcheck.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -97,7 +97,7 @@
   \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
 
-instantiation "fun" :: ("{eq, term_of}", random) random
+instantiation "fun" :: ("{equal, term_of}", random) random
 begin
 
 definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Rat.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -1083,18 +1083,18 @@
   by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
 qed
 
-instantiation rat :: eq
+instantiation rat :: equal
 begin
 
 definition [code]:
-  "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b"
+  "HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b"
 
 instance proof
-qed (simp add: eq_rat_def quotient_of_inject_eq)
+qed (simp add: equal_rat_def quotient_of_inject_eq)
 
 lemma rat_eq_refl [code nbe]:
-  "eq_class.eq (r::rat) r \<longleftrightarrow> True"
-  by (rule HOL.eq_refl)
+  "HOL.equal (r::rat) r \<longleftrightarrow> True"
+  by (rule equal_refl)
 
 end
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/RealDef.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -1697,19 +1697,21 @@
   "Ratreal (number_of r / number_of s) = number_of r / number_of s"
 unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
 
-instantiation real :: eq
+instantiation real :: equal
 begin
 
-definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
+definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
 
-instance by default (simp add: eq_real_def)
+instance proof
+qed (simp add: equal_real_def)
 
-lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq x y"
-  by (simp add: eq_real_def eq)
+lemma real_equal_code [code]:
+  "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
+  by (simp add: equal_real_def equal)
 
-lemma real_eq_refl [code nbe]:
-  "eq_class.eq (x::real) x \<longleftrightarrow> True"
-  by (rule HOL.eq_refl)
+lemma [code nbe]:
+  "HOL.equal (x::real) x \<longleftrightarrow> True"
+  by (rule equal_refl)
 
 end
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/String.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -183,10 +183,10 @@
   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
 *}
 
-code_instance literal :: eq
+code_instance literal :: equal
   (Haskell -)
 
-code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
   (OCaml "!((_ : string) = _)")
   (Haskell infixl 4 "==")
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Aug 27 19:34:23 2010 +0200
@@ -68,7 +68,7 @@
     val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
       Datatype_Data.the_info thy tyco;
     val ty = Type (tyco, map TFree vs);
-    fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+    fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT)
       $ t1 $ t2;
     fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
     fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
@@ -83,7 +83,7 @@
     val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
     val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps 
-      (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
+      (map Simpdata.mk_eq (@{thm equal} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
     fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
       |> Simpdata.mk_eq;
   in (map prove (triv_injects @ injects @ distincts), prove refl) end;
@@ -96,7 +96,7 @@
         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
           $ Free ("x", ty) $ Free ("y", ty);
         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
-          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
+          (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
           (NONE, (Attrib.empty_binding, def')) lthy;
@@ -115,7 +115,7 @@
       #> snd
   in
     thy
-    |> Class.instantiation (tycos, vs, [HOLogic.class_eq])
+    |> Class.instantiation (tycos, vs, [HOLogic.class_equal])
     |> fold_map add_def tycos
     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
          (fn _ => fn def_thms => tac def_thms) def_thms)
@@ -135,7 +135,7 @@
     val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
     val certs = map (mk_case_cert thy) tycos;
     val tycos_eq = filter_out
-      (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_eq]) tycos;
+      (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
   in
     if null css then thy
     else thy
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Aug 27 19:34:23 2010 +0200
@@ -182,7 +182,7 @@
 fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
 
 val syntactic_sorts =
-  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
+  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
   @{sort number}
 fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
     subset (op =) (S, syntactic_sorts)
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Fri Aug 27 19:34:23 2010 +0200
@@ -49,7 +49,7 @@
   val exists_const: typ -> term
   val mk_exists: string * typ * term -> term
   val choice_const: typ -> term
-  val class_eq: string
+  val class_equal: string
   val mk_binop: string -> term * term -> term
   val mk_binrel: string -> term * term -> term
   val dest_bin: string -> typ -> term -> term * term
@@ -251,7 +251,7 @@
 
 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
 
-val class_eq = "HOL.eq";
+val class_equal = "HOL.equal";
 
 
 (* binary operations and relations *)
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Tools/record.ML	Fri Aug 27 19:34:23 2010 +0200
@@ -1844,7 +1844,7 @@
   let
     val eq =
       (HOLogic.mk_Trueprop o HOLogic.mk_eq)
-        (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
+        (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
          Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
     fun tac eq_def =
       Class.intro_classes_tac []
@@ -1853,15 +1853,15 @@
     fun mk_eq thy eq_def = Simplifier.rewrite_rule
       [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
     fun mk_eq_refl thy =
-      @{thm HOL.eq_refl}
+      @{thm equal_refl}
       |> Thm.instantiate
-        ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
+        ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
       |> AxClass.unoverload thy;
   in
     thy
     |> Code.add_datatype [ext]
     |> fold Code.add_default_eqn simps
-    |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_eq])
+    |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition
          (NONE, (Attrib.empty_binding, eq)))
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Typerep.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -78,9 +78,13 @@
 *}
 
 lemma [code]:
-  "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
-     \<and> list_all2 eq_class.eq tys1 tys2"
-  by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
+  "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
+     \<and> list_all2 HOL.equal tys1 tys2"
+  by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
+
+lemma [code nbe]:
+  "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 code_type typerep
   (Eval "Term.typ")
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Word/Word.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -953,14 +953,14 @@
 
 text {* Executable equality *}
 
-instantiation word :: ("{len0}") eq
+instantiation word :: (len0) equal
 begin
 
-definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
-  "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+  "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
 
 instance proof
-qed (simp add: eq eq_word_def)
+qed (simp add: equal equal_word_def)
 
 end
 
diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -845,7 +845,7 @@
   "(uminus :: int \<Rightarrow> int) = uminus"
   "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
   "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
-  "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
+  "(HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool) = HOL.equal"
   "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
   "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
   by rule+
@@ -928,16 +928,20 @@
   by simp_all
 
 lemma eq_int_code [code]:
-  "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
-  "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
-  "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
-  "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
-  "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
-  "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
-  "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
-  "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
-  "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
-  by (auto simp add: eq dest: sym)
+  "HOL.equal 0 (0::int) \<longleftrightarrow> True"
+  "HOL.equal 0 (Pls l) \<longleftrightarrow> False"
+  "HOL.equal 0 (Mns l) \<longleftrightarrow> False"
+  "HOL.equal (Pls k) 0 \<longleftrightarrow> False"
+  "HOL.equal (Pls k) (Pls l) \<longleftrightarrow> HOL.equal k l"
+  "HOL.equal (Pls k) (Mns l) \<longleftrightarrow> False"
+  "HOL.equal (Mns k) 0 \<longleftrightarrow> False"
+  "HOL.equal (Mns k) (Pls l) \<longleftrightarrow> False"
+  "HOL.equal (Mns k) (Mns l) \<longleftrightarrow> HOL.equal k l"
+  by (auto simp add: equal dest: sym)
+
+lemma [code nbe]:
+  "HOL.equal (k::int) k \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 lemma less_eq_int_code [code]:
   "0 \<le> (0::int) \<longleftrightarrow> True"
@@ -1078,7 +1082,7 @@
   (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
 
-code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")