merged
authorhaftmann
Sat Aug 28 11:42:33 2010 +0200 (2010-08-28)
changeset 388581920158cfa17
parent 38838 62f6ba39b3d4
parent 38857 97775f3e8722
child 38859 053c69cb4a0e
merged
NEWS
src/HOL/String.thy
     1.1 --- a/NEWS	Fri Aug 27 22:30:25 2010 +0200
     1.2 +++ b/NEWS	Sat Aug 28 11:42:33 2010 +0200
     1.3 @@ -62,6 +62,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Renamed class eq and constant eq (for code generation) to class equal
     1.8 +and constant equal, plus renaming of related facts and various tuning.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Scala (2.8 or higher) has been added to the target languages of
    1.12  the code generator.
    1.13  
     2.1 --- a/doc-src/Codegen/Thy/Foundations.thy	Fri Aug 27 22:30:25 2010 +0200
     2.2 +++ b/doc-src/Codegen/Thy/Foundations.thy	Sat Aug 28 11:42:33 2010 +0200
     2.3 @@ -220,12 +220,12 @@
     2.4  text {*
     2.5    \noindent Obviously, polymorphic equality is implemented the Haskell
     2.6    way using a type class.  How is this achieved?  HOL introduces an
     2.7 -  explicit class @{class eq} with a corresponding operation @{const
     2.8 -  eq_class.eq} such that @{thm eq [no_vars]}.  The preprocessing
     2.9 -  framework does the rest by propagating the @{class eq} constraints
    2.10 +  explicit class @{class equal} with a corresponding operation @{const
    2.11 +  HOL.equal} such that @{thm equal [no_vars]}.  The preprocessing
    2.12 +  framework does the rest by propagating the @{class equal} constraints
    2.13    through all dependent code equations.  For datatypes, instances of
    2.14 -  @{class eq} are implicitly derived when possible.  For other types,
    2.15 -  you may instantiate @{text eq} manually like any other type class.
    2.16 +  @{class equal} are implicitly derived when possible.  For other types,
    2.17 +  you may instantiate @{text equal} manually like any other type class.
    2.18  *}
    2.19  
    2.20  
     3.1 --- a/src/HOL/Code_Evaluation.thy	Fri Aug 27 22:30:25 2010 +0200
     3.2 +++ b/src/HOL/Code_Evaluation.thy	Sat Aug 28 11:42:33 2010 +0200
     3.3 @@ -162,7 +162,7 @@
     3.4  subsubsection {* Code generator setup *}
     3.5  
     3.6  lemmas [code del] = term.recs term.cases term.size
     3.7 -lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
     3.8 +lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
     3.9  
    3.10  lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
    3.11  lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
     4.1 --- a/src/HOL/Code_Numeral.thy	Fri Aug 27 22:30:25 2010 +0200
     4.2 +++ b/src/HOL/Code_Numeral.thy	Sat Aug 28 11:42:33 2010 +0200
     4.3 @@ -115,12 +115,12 @@
     4.4  lemmas [code del] = code_numeral.recs code_numeral.cases
     4.5  
     4.6  lemma [code]:
     4.7 -  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
     4.8 -  by (cases k, cases l) (simp add: eq)
     4.9 +  "HOL.equal k l \<longleftrightarrow> HOL.equal (nat_of k) (nat_of l)"
    4.10 +  by (cases k, cases l) (simp add: equal)
    4.11  
    4.12  lemma [code nbe]:
    4.13 -  "eq_class.eq (k::code_numeral) k \<longleftrightarrow> True"
    4.14 -  by (rule HOL.eq_refl)
    4.15 +  "HOL.equal (k::code_numeral) k \<longleftrightarrow> True"
    4.16 +  by (rule equal_refl)
    4.17  
    4.18  
    4.19  subsection {* Code numerals as datatype of ints *}
    4.20 @@ -301,7 +301,7 @@
    4.21    (Haskell "Integer")
    4.22    (Scala "BigInt")
    4.23  
    4.24 -code_instance code_numeral :: eq
    4.25 +code_instance code_numeral :: equal
    4.26    (Haskell -)
    4.27  
    4.28  setup {*
    4.29 @@ -342,7 +342,7 @@
    4.30    (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
    4.31    (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    4.32  
    4.33 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    4.34 +code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    4.35    (SML "!((_ : Int.int) = _)")
    4.36    (OCaml "Big'_int.eq'_big'_int")
    4.37    (Haskell infixl 4 "==")
     5.1 --- a/src/HOL/HOL.thy	Fri Aug 27 22:30:25 2010 +0200
     5.2 +++ b/src/HOL/HOL.thy	Sat Aug 28 11:42:33 2010 +0200
     5.3 @@ -1775,31 +1775,30 @@
     5.4  
     5.5  subsubsection {* Equality *}
     5.6  
     5.7 -class eq =
     5.8 -  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     5.9 -  assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    5.10 +class equal =
    5.11 +  fixes equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.12 +  assumes equal_eq: "equal x y \<longleftrightarrow> x = y"
    5.13  begin
    5.14  
    5.15 -lemma eq [code_unfold, code_inline del]: "eq = (op =)"
    5.16 -  by (rule ext eq_equals)+
    5.17 +lemma equal [code_unfold, code_inline del]: "equal = (op =)"
    5.18 +  by (rule ext equal_eq)+
    5.19  
    5.20 -lemma eq_refl: "eq x x \<longleftrightarrow> True"
    5.21 -  unfolding eq by rule+
    5.22 +lemma equal_refl: "equal x x \<longleftrightarrow> True"
    5.23 +  unfolding equal by rule+
    5.24  
    5.25 -lemma equals_eq: "(op =) \<equiv> eq"
    5.26 -  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
    5.27 -
    5.28 -declare equals_eq [symmetric, code_post]
    5.29 +lemma eq_equal: "(op =) \<equiv> equal"
    5.30 +  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule equal_eq)
    5.31  
    5.32  end
    5.33  
    5.34 -declare equals_eq [code]
    5.35 +declare eq_equal [symmetric, code_post]
    5.36 +declare eq_equal [code]
    5.37  
    5.38  setup {*
    5.39    Code_Preproc.map_pre (fn simpset =>
    5.40 -    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "eq" [@{term "op ="}]
    5.41 +    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term "op ="}]
    5.42        (fn thy => fn _ => fn Const (_, T) => case strip_type T
    5.43 -        of (Type _ :: _, _) => SOME @{thm equals_eq}
    5.44 +        of (Type _ :: _, _) => SOME @{thm eq_equal}
    5.45           | _ => NONE)])
    5.46  *}
    5.47  
    5.48 @@ -1839,50 +1838,50 @@
    5.49      and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
    5.50      and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all
    5.51  
    5.52 -instantiation itself :: (type) eq
    5.53 +instantiation itself :: (type) equal
    5.54  begin
    5.55  
    5.56 -definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
    5.57 -  "eq_itself x y \<longleftrightarrow> x = y"
    5.58 +definition equal_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where
    5.59 +  "equal_itself x y \<longleftrightarrow> x = y"
    5.60  
    5.61  instance proof
    5.62 -qed (fact eq_itself_def)
    5.63 +qed (fact equal_itself_def)
    5.64  
    5.65  end
    5.66  
    5.67 -lemma eq_itself_code [code]:
    5.68 -  "eq_class.eq TYPE('a) TYPE('a) \<longleftrightarrow> True"
    5.69 -  by (simp add: eq)
    5.70 +lemma equal_itself_code [code]:
    5.71 +  "equal TYPE('a) TYPE('a) \<longleftrightarrow> True"
    5.72 +  by (simp add: equal)
    5.73  
    5.74  text {* Equality *}
    5.75  
    5.76  declare simp_thms(6) [code nbe]
    5.77  
    5.78  setup {*
    5.79 -  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
    5.80 +  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>type \<Rightarrow> 'a \<Rightarrow> bool"})
    5.81  *}
    5.82  
    5.83 -lemma equals_alias_cert: "OFCLASS('a, eq_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> eq)" (is "?ofclass \<equiv> ?eq")
    5.84 +lemma equal_alias_cert: "OFCLASS('a, equal_class) \<equiv> ((op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool) \<equiv> equal)" (is "?ofclass \<equiv> ?equal")
    5.85  proof
    5.86    assume "PROP ?ofclass"
    5.87 -  show "PROP ?eq"
    5.88 -    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *})
    5.89 +  show "PROP ?equal"
    5.90 +    by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
    5.91        (fact `PROP ?ofclass`)
    5.92  next
    5.93 -  assume "PROP ?eq"
    5.94 +  assume "PROP ?equal"
    5.95    show "PROP ?ofclass" proof
    5.96 -  qed (simp add: `PROP ?eq`)
    5.97 +  qed (simp add: `PROP ?equal`)
    5.98  qed
    5.99    
   5.100  setup {*
   5.101 -  Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\<Colon>eq \<Rightarrow> 'a \<Rightarrow> bool"})
   5.102 +  Sign.add_const_constraint (@{const_name equal}, SOME @{typ "'a\<Colon>equal \<Rightarrow> 'a \<Rightarrow> bool"})
   5.103  *}
   5.104  
   5.105  setup {*
   5.106 -  Nbe.add_const_alias @{thm equals_alias_cert}
   5.107 +  Nbe.add_const_alias @{thm equal_alias_cert}
   5.108  *}
   5.109  
   5.110 -hide_const (open) eq
   5.111 +hide_const (open) equal
   5.112  
   5.113  text {* Cases *}
   5.114  
   5.115 @@ -1939,10 +1938,10 @@
   5.116  
   5.117  text {* using built-in Haskell equality *}
   5.118  
   5.119 -code_class eq
   5.120 +code_class equal
   5.121    (Haskell "Eq")
   5.122  
   5.123 -code_const "eq_class.eq"
   5.124 +code_const "HOL.equal"
   5.125    (Haskell infixl 4 "==")
   5.126  
   5.127  code_const "op ="
     6.1 --- a/src/HOL/Int.thy	Fri Aug 27 22:30:25 2010 +0200
     6.2 +++ b/src/HOL/Int.thy	Sat Aug 28 11:42:33 2010 +0200
     6.3 @@ -2222,42 +2222,42 @@
     6.4    mult_bin_simps
     6.5    arith_extra_simps(4) [where 'a = int]
     6.6  
     6.7 -instantiation int :: eq
     6.8 +instantiation int :: equal
     6.9  begin
    6.10  
    6.11  definition
    6.12 -  "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
    6.13 -
    6.14 -instance by default (simp add: eq_int_def)
    6.15 +  "HOL.equal k l \<longleftrightarrow> k - l = (0\<Colon>int)"
    6.16 +
    6.17 +instance by default (simp add: equal_int_def)
    6.18  
    6.19  end
    6.20  
    6.21  lemma eq_number_of_int_code [code]:
    6.22 -  "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
    6.23 -  unfolding eq_int_def number_of_is_id ..
    6.24 +  "HOL.equal (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> HOL.equal k l"
    6.25 +  unfolding equal_int_def number_of_is_id ..
    6.26  
    6.27  lemma eq_int_code [code]:
    6.28 -  "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
    6.29 -  "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
    6.30 -  "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
    6.31 -  "eq_class.eq Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
    6.32 -  "eq_class.eq Int.Min Int.Pls \<longleftrightarrow> False"
    6.33 -  "eq_class.eq Int.Min Int.Min \<longleftrightarrow> True"
    6.34 -  "eq_class.eq Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
    6.35 -  "eq_class.eq Int.Min (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq Int.Min k2"
    6.36 -  "eq_class.eq (Int.Bit0 k1) Int.Pls \<longleftrightarrow> eq_class.eq k1 Int.Pls"
    6.37 -  "eq_class.eq (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
    6.38 -  "eq_class.eq (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
    6.39 -  "eq_class.eq (Int.Bit1 k1) Int.Min \<longleftrightarrow> eq_class.eq k1 Int.Min"
    6.40 -  "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq k1 k2"
    6.41 -  "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
    6.42 -  "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
    6.43 -  "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> eq_class.eq k1 k2"
    6.44 -  unfolding eq_equals by simp_all
    6.45 +  "HOL.equal Int.Pls Int.Pls \<longleftrightarrow> True"
    6.46 +  "HOL.equal Int.Pls Int.Min \<longleftrightarrow> False"
    6.47 +  "HOL.equal Int.Pls (Int.Bit0 k2) \<longleftrightarrow> HOL.equal Int.Pls k2"
    6.48 +  "HOL.equal Int.Pls (Int.Bit1 k2) \<longleftrightarrow> False"
    6.49 +  "HOL.equal Int.Min Int.Pls \<longleftrightarrow> False"
    6.50 +  "HOL.equal Int.Min Int.Min \<longleftrightarrow> True"
    6.51 +  "HOL.equal Int.Min (Int.Bit0 k2) \<longleftrightarrow> False"
    6.52 +  "HOL.equal Int.Min (Int.Bit1 k2) \<longleftrightarrow> HOL.equal Int.Min k2"
    6.53 +  "HOL.equal (Int.Bit0 k1) Int.Pls \<longleftrightarrow> HOL.equal k1 Int.Pls"
    6.54 +  "HOL.equal (Int.Bit1 k1) Int.Pls \<longleftrightarrow> False"
    6.55 +  "HOL.equal (Int.Bit0 k1) Int.Min \<longleftrightarrow> False"
    6.56 +  "HOL.equal (Int.Bit1 k1) Int.Min \<longleftrightarrow> HOL.equal k1 Int.Min"
    6.57 +  "HOL.equal (Int.Bit0 k1) (Int.Bit0 k2) \<longleftrightarrow> HOL.equal k1 k2"
    6.58 +  "HOL.equal (Int.Bit0 k1) (Int.Bit1 k2) \<longleftrightarrow> False"
    6.59 +  "HOL.equal (Int.Bit1 k1) (Int.Bit0 k2) \<longleftrightarrow> False"
    6.60 +  "HOL.equal (Int.Bit1 k1) (Int.Bit1 k2) \<longleftrightarrow> HOL.equal k1 k2"
    6.61 +  unfolding equal_eq by simp_all
    6.62  
    6.63  lemma eq_int_refl [code nbe]:
    6.64 -  "eq_class.eq (k::int) k \<longleftrightarrow> True"
    6.65 -  by (rule HOL.eq_refl)
    6.66 +  "HOL.equal (k::int) k \<longleftrightarrow> True"
    6.67 +  by (rule equal_refl)
    6.68  
    6.69  lemma less_eq_number_of_int_code [code]:
    6.70    "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
     7.1 --- a/src/HOL/Lazy_Sequence.thy	Fri Aug 27 22:30:25 2010 +0200
     7.2 +++ b/src/HOL/Lazy_Sequence.thy	Sat Aug 28 11:42:33 2010 +0200
     7.3 @@ -39,10 +39,14 @@
     7.4    "size xq = (case yield xq of None => 0 | Some (x, xq') => size xq' + 1)"
     7.5  by (cases xq) auto
     7.6  
     7.7 -lemma [code]: "eq_class.eq xq yq = (case (yield xq, yield yq) of
     7.8 -  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.eq x y) \<and> (eq_class.eq xq yq) | _ => False)"
     7.9 -apply (cases xq) apply (cases yq) apply (auto simp add: eq_class.eq_equals) 
    7.10 -apply (cases yq) apply (auto simp add: eq_class.eq_equals) done
    7.11 +lemma [code]: "HOL.equal xq yq = (case (yield xq, yield yq) of
    7.12 +  (None, None) => True | (Some (x, xq'), Some (y, yq')) => (HOL.equal x y) \<and> (HOL.equal xq yq) | _ => False)"
    7.13 +apply (cases xq) apply (cases yq) apply (auto simp add: equal_eq) 
    7.14 +apply (cases yq) apply (auto simp add: equal_eq) done
    7.15 +
    7.16 +lemma [code nbe]:
    7.17 +  "HOL.equal (x :: 'a lazy_sequence) x \<longleftrightarrow> True"
    7.18 +  by (fact equal_refl)
    7.19  
    7.20  lemma seq_case [code]:
    7.21    "lazy_sequence_case f g xq = (case (yield xq) of None => f | Some (x, xq') => g x xq')"
     8.1 --- a/src/HOL/Library/AssocList.thy	Fri Aug 27 22:30:25 2010 +0200
     8.2 +++ b/src/HOL/Library/AssocList.thy	Sat Aug 28 11:42:33 2010 +0200
     8.3 @@ -701,7 +701,44 @@
     8.4    "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
     8.5    by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
     8.6  
     8.7 -lemma [code, code del]:
     8.8 -  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
     8.9 +lemma map_of_eqI: (*FIXME move to Map.thy*)
    8.10 +  assumes set_eq: "set (map fst xs) = set (map fst ys)"
    8.11 +  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
    8.12 +  shows "map_of xs = map_of ys"
    8.13 +proof (rule ext)
    8.14 +  fix k show "map_of xs k = map_of ys k"
    8.15 +  proof (cases "map_of xs k")
    8.16 +    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
    8.17 +    with set_eq have "k \<notin> set (map fst ys)" by simp
    8.18 +    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
    8.19 +    with None show ?thesis by simp
    8.20 +  next
    8.21 +    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
    8.22 +    with map_eq show ?thesis by auto
    8.23 +  qed
    8.24 +qed
    8.25 +
    8.26 +lemma map_of_eq_dom: (*FIXME move to Map.thy*)
    8.27 +  assumes "map_of xs = map_of ys"
    8.28 +  shows "fst ` set xs = fst ` set ys"
    8.29 +proof -
    8.30 +  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
    8.31 +  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
    8.32 +qed
    8.33 +
    8.34 +lemma equal_Mapping [code]:
    8.35 +  "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
    8.36 +    (let ks = map fst xs; ls = map fst ys
    8.37 +    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))"
    8.38 +proof -
    8.39 +  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)
    8.40 +  show ?thesis
    8.41 +    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
    8.42 +      (auto dest!: map_of_eq_dom intro: aux)
    8.43 +qed
    8.44 +
    8.45 +lemma [code nbe]:
    8.46 +  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
    8.47 +  by (fact equal_refl)
    8.48  
    8.49  end
     9.1 --- a/src/HOL/Library/Code_Char.thy	Fri Aug 27 22:30:25 2010 +0200
     9.2 +++ b/src/HOL/Library/Code_Char.thy	Sat Aug 28 11:42:33 2010 +0200
     9.3 @@ -19,7 +19,7 @@
     9.4    #> String_Code.add_literal_list_string "Haskell"
     9.5  *}
     9.6  
     9.7 -code_instance char :: eq
     9.8 +code_instance char :: equal
     9.9    (Haskell -)
    9.10  
    9.11  code_reserved SML
    9.12 @@ -31,7 +31,7 @@
    9.13  code_reserved Scala
    9.14    char
    9.15  
    9.16 -code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    9.17 +code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    9.18    (SML "!((_ : char) = _)")
    9.19    (OCaml "!((_ : char) = _)")
    9.20    (Haskell infixl 4 "==")
    10.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Aug 27 22:30:25 2010 +0200
    10.2 +++ b/src/HOL/Library/Code_Integer.thy	Sat Aug 28 11:42:33 2010 +0200
    10.3 @@ -21,7 +21,7 @@
    10.4    (Scala "BigInt")
    10.5    (Eval "int")
    10.6  
    10.7 -code_instance int :: eq
    10.8 +code_instance int :: equal
    10.9    (Haskell -)
   10.10  
   10.11  setup {*
   10.12 @@ -96,7 +96,7 @@
   10.13    (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   10.14    (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
   10.15  
   10.16 -code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   10.17 +code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   10.18    (SML "!((_ : IntInf.int) = _)")
   10.19    (OCaml "Big'_int.eq'_big'_int")
   10.20    (Haskell infixl 4 "==")
    11.1 --- a/src/HOL/Library/Code_Natural.thy	Fri Aug 27 22:30:25 2010 +0200
    11.2 +++ b/src/HOL/Library/Code_Natural.thy	Sat Aug 28 11:42:33 2010 +0200
    11.3 @@ -112,7 +112,7 @@
    11.4      false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
    11.5  *}
    11.6  
    11.7 -code_instance code_numeral :: eq
    11.8 +code_instance code_numeral :: equal
    11.9    (Haskell -)
   11.10  
   11.11  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   11.12 @@ -131,7 +131,7 @@
   11.13    (Haskell "divMod")
   11.14    (Scala infixl 8 "/%")
   11.15  
   11.16 -code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   11.17 +code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   11.18    (Haskell infixl 4 "==")
   11.19    (Scala infixl 5 "==")
   11.20  
    12.1 --- a/src/HOL/Library/Dlist.thy	Fri Aug 27 22:30:25 2010 +0200
    12.2 +++ b/src/HOL/Library/Dlist.thy	Sat Aug 28 11:42:33 2010 +0200
    12.3 @@ -109,16 +109,20 @@
    12.4  
    12.5  text {* Equality *}
    12.6  
    12.7 -instantiation dlist :: (eq) eq
    12.8 +instantiation dlist :: (equal) equal
    12.9  begin
   12.10  
   12.11 -definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
   12.12 +definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
   12.13  
   12.14  instance proof
   12.15 -qed (simp add: eq_dlist_def eq list_of_dlist_inject)
   12.16 +qed (simp add: equal_dlist_def equal list_of_dlist_inject)
   12.17  
   12.18  end
   12.19  
   12.20 +lemma [code nbe]:
   12.21 +  "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
   12.22 +  by (fact equal_refl)
   12.23 +
   12.24  
   12.25  section {* Induction principle and case distinction *}
   12.26  
    13.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 27 22:30:25 2010 +0200
    13.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Sat Aug 28 11:42:33 2010 +0200
    13.3 @@ -55,12 +55,12 @@
    13.4    by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
    13.5  
    13.6  lemma eq_nat_code [code]:
    13.7 -  "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
    13.8 -  by (simp add: eq)
    13.9 +  "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
   13.10 +  by (simp add: equal)
   13.11  
   13.12  lemma eq_nat_refl [code nbe]:
   13.13 -  "eq_class.eq (n::nat) n \<longleftrightarrow> True"
   13.14 -  by (rule HOL.eq_refl)
   13.15 +  "HOL.equal (n::nat) n \<longleftrightarrow> True"
   13.16 +  by (rule equal_refl)
   13.17  
   13.18  lemma less_eq_nat_code [code]:
   13.19    "n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
   13.20 @@ -332,7 +332,7 @@
   13.21    (Haskell "Nat.Nat")
   13.22    (Scala "Nat.Nat")
   13.23  
   13.24 -code_instance nat :: eq
   13.25 +code_instance nat :: equal
   13.26    (Haskell -)
   13.27  
   13.28  text {*
   13.29 @@ -442,7 +442,7 @@
   13.30    (Scala infixl 8 "/%")
   13.31    (Eval "Integer.div'_mod")
   13.32  
   13.33 -code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   13.34 +code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   13.35    (SML "!((_ : IntInf.int) = _)")
   13.36    (OCaml "Big'_int.eq'_big'_int")
   13.37    (Haskell infixl 4 "==")
    14.1 --- a/src/HOL/Library/Enum.thy	Fri Aug 27 22:30:25 2010 +0200
    14.2 +++ b/src/HOL/Library/Enum.thy	Sat Aug 28 11:42:33 2010 +0200
    14.3 @@ -35,17 +35,21 @@
    14.4  
    14.5  subsection {* Equality and order on functions *}
    14.6  
    14.7 -instantiation "fun" :: (enum, eq) eq
    14.8 +instantiation "fun" :: (enum, equal) equal
    14.9  begin
   14.10  
   14.11  definition
   14.12 -  "eq_class.eq f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
   14.13 +  "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
   14.14  
   14.15  instance proof
   14.16 -qed (simp_all add: eq_fun_def enum_all expand_fun_eq)
   14.17 +qed (simp_all add: equal_fun_def enum_all expand_fun_eq)
   14.18  
   14.19  end
   14.20  
   14.21 +lemma [code nbe]:
   14.22 +  "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
   14.23 +  by (fact equal_refl)
   14.24 +
   14.25  lemma order_fun [code]:
   14.26    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   14.27    shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
   14.28 @@ -169,7 +173,7 @@
   14.29  
   14.30  end
   14.31  
   14.32 -lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
   14.33 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
   14.34    in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   14.35    by (simp add: enum_fun_def Let_def)
   14.36  
    15.1 --- a/src/HOL/Library/Fset.thy	Fri Aug 27 22:30:25 2010 +0200
    15.2 +++ b/src/HOL/Library/Fset.thy	Sat Aug 28 11:42:33 2010 +0200
    15.3 @@ -227,17 +227,21 @@
    15.4    "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
    15.5    by (fact less_le_not_le)
    15.6  
    15.7 -instantiation fset :: (type) eq
    15.8 +instantiation fset :: (type) equal
    15.9  begin
   15.10  
   15.11  definition
   15.12 -  "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
   15.13 +  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
   15.14  
   15.15  instance proof
   15.16 -qed (simp add: eq_fset_def set_eq [symmetric])
   15.17 +qed (simp add: equal_fset_def set_eq [symmetric])
   15.18  
   15.19  end
   15.20  
   15.21 +lemma [code nbe]:
   15.22 +  "HOL.equal (A :: 'a fset) A \<longleftrightarrow> True"
   15.23 +  by (fact equal_refl)
   15.24 +
   15.25  
   15.26  subsection {* Functorial operations *}
   15.27  
    16.1 --- a/src/HOL/Library/List_Prefix.thy	Fri Aug 27 22:30:25 2010 +0200
    16.2 +++ b/src/HOL/Library/List_Prefix.thy	Sat Aug 28 11:42:33 2010 +0200
    16.3 @@ -81,9 +81,9 @@
    16.4    by (auto simp add: prefix_def)
    16.5  
    16.6  lemma less_eq_list_code [code]:
    16.7 -  "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
    16.8 -  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
    16.9 -  "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   16.10 +  "([]\<Colon>'a\<Colon>{equal, ord} list) \<le> xs \<longleftrightarrow> True"
   16.11 +  "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> [] \<longleftrightarrow> False"
   16.12 +  "(x\<Colon>'a\<Colon>{equal, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   16.13    by simp_all
   16.14  
   16.15  lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)"
    17.1 --- a/src/HOL/Library/List_lexord.thy	Fri Aug 27 22:30:25 2010 +0200
    17.2 +++ b/src/HOL/Library/List_lexord.thy	Sat Aug 28 11:42:33 2010 +0200
    17.3 @@ -103,15 +103,15 @@
    17.4  end
    17.5  
    17.6  lemma less_list_code [code]:
    17.7 -  "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
    17.8 -  "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
    17.9 -  "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
   17.10 +  "xs < ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
   17.11 +  "[] < (x\<Colon>'a\<Colon>{equal, order}) # xs \<longleftrightarrow> True"
   17.12 +  "(x\<Colon>'a\<Colon>{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
   17.13    by simp_all
   17.14  
   17.15  lemma less_eq_list_code [code]:
   17.16 -  "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   17.17 -  "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
   17.18 -  "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
   17.19 +  "x # xs \<le> ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
   17.20 +  "[] \<le> (xs\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> True"
   17.21 +  "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
   17.22    by simp_all
   17.23  
   17.24  end
    18.1 --- a/src/HOL/Library/Mapping.thy	Fri Aug 27 22:30:25 2010 +0200
    18.2 +++ b/src/HOL/Library/Mapping.thy	Sat Aug 28 11:42:33 2010 +0200
    18.3 @@ -280,14 +280,14 @@
    18.4  
    18.5  code_datatype empty update
    18.6  
    18.7 -instantiation mapping :: (type, type) eq
    18.8 +instantiation mapping :: (type, type) equal
    18.9  begin
   18.10  
   18.11  definition [code del]:
   18.12 -  "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
   18.13 +  "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
   18.14  
   18.15  instance proof
   18.16 -qed (simp add: eq_mapping_def)
   18.17 +qed (simp add: equal_mapping_def)
   18.18  
   18.19  end
   18.20  
    19.1 --- a/src/HOL/Library/Multiset.thy	Fri Aug 27 22:30:25 2010 +0200
    19.2 +++ b/src/HOL/Library/Multiset.thy	Sat Aug 28 11:42:33 2010 +0200
    19.3 @@ -938,17 +938,21 @@
    19.4    qed
    19.5  qed
    19.6  
    19.7 -instantiation multiset :: (eq) eq
    19.8 +instantiation multiset :: (equal) equal
    19.9  begin
   19.10  
   19.11  definition
   19.12 -  "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
   19.13 +  "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
   19.14  
   19.15  instance proof
   19.16 -qed (simp add: eq_multiset_def eq_iff)
   19.17 +qed (simp add: equal_multiset_def eq_iff)
   19.18  
   19.19  end
   19.20  
   19.21 +lemma [code nbe]:
   19.22 +  "HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True"
   19.23 +  by (fact equal_refl)
   19.24 +
   19.25  definition (in term_syntax)
   19.26    bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
   19.27      \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    20.1 --- a/src/HOL/Library/Nested_Environment.thy	Fri Aug 27 22:30:25 2010 +0200
    20.2 +++ b/src/HOL/Library/Nested_Environment.thy	Sat Aug 28 11:42:33 2010 +0200
    20.3 @@ -521,22 +521,21 @@
    20.4  text {* Environments and code generation *}
    20.5  
    20.6  lemma [code, code del]:
    20.7 -  fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
    20.8 -  shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
    20.9 +  "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
   20.10  
   20.11 -lemma eq_env_code [code]:
   20.12 -  fixes x y :: "'a\<Colon>eq"
   20.13 -    and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
   20.14 -  shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
   20.15 -  eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
   20.16 +lemma equal_env_code [code]:
   20.17 +  fixes x y :: "'a\<Colon>equal"
   20.18 +    and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
   20.19 +  shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
   20.20 +  HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
   20.21     of None \<Rightarrow> (case g z
   20.22          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   20.23      | Some a \<Rightarrow> (case g z
   20.24 -        of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
   20.25 -    and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
   20.26 -    and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
   20.27 -    and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
   20.28 -proof (unfold eq)
   20.29 +        of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
   20.30 +    and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
   20.31 +    and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
   20.32 +    and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
   20.33 +proof (unfold equal)
   20.34    have "f = g \<longleftrightarrow> (\<forall>z. case f z
   20.35     of None \<Rightarrow> (case g z
   20.36          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   20.37 @@ -562,6 +561,10 @@
   20.38            of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
   20.39  qed simp_all
   20.40  
   20.41 +lemma [code nbe]:
   20.42 +  "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
   20.43 +  by (fact equal_refl)
   20.44 +
   20.45  lemma [code, code del]:
   20.46    "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
   20.47  
    21.1 --- a/src/HOL/Library/Polynomial.thy	Fri Aug 27 22:30:25 2010 +0200
    21.2 +++ b/src/HOL/Library/Polynomial.thy	Sat Aug 28 11:42:33 2010 +0200
    21.3 @@ -1505,23 +1505,27 @@
    21.4  
    21.5  declare pCons_0_0 [code_post]
    21.6  
    21.7 -instantiation poly :: ("{zero,eq}") eq
    21.8 +instantiation poly :: ("{zero, equal}") equal
    21.9  begin
   21.10  
   21.11  definition
   21.12 -  "eq_class.eq (p::'a poly) q \<longleftrightarrow> p = q"
   21.13 +  "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q"
   21.14  
   21.15 -instance
   21.16 -  by default (rule eq_poly_def)
   21.17 +instance proof
   21.18 +qed (rule equal_poly_def)
   21.19  
   21.20  end
   21.21  
   21.22  lemma eq_poly_code [code]:
   21.23 -  "eq_class.eq (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
   21.24 -  "eq_class.eq (0::_ poly) (pCons b q) \<longleftrightarrow> eq_class.eq 0 b \<and> eq_class.eq 0 q"
   21.25 -  "eq_class.eq (pCons a p) (0::_ poly) \<longleftrightarrow> eq_class.eq a 0 \<and> eq_class.eq p 0"
   21.26 -  "eq_class.eq (pCons a p) (pCons b q) \<longleftrightarrow> eq_class.eq a b \<and> eq_class.eq p q"
   21.27 -unfolding eq by simp_all
   21.28 +  "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True"
   21.29 +  "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q"
   21.30 +  "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0"
   21.31 +  "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q"
   21.32 +  by (simp_all add: equal)
   21.33 +
   21.34 +lemma [code nbe]:
   21.35 +  "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
   21.36 +  by (fact equal_refl)
   21.37  
   21.38  lemmas coeff_code [code] =
   21.39    coeff_0 coeff_pCons_0 coeff_pCons_Suc
    22.1 --- a/src/HOL/Library/Product_ord.thy	Fri Aug 27 22:30:25 2010 +0200
    22.2 +++ b/src/HOL/Library/Product_ord.thy	Sat Aug 28 11:42:33 2010 +0200
    22.3 @@ -22,8 +22,8 @@
    22.4  end
    22.5  
    22.6  lemma [code]:
    22.7 -  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
    22.8 -  "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
    22.9 +  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 \<le> y2"
   22.10 +  "(x1\<Colon>'a\<Colon>{ord, equal}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 \<le> x2 \<and> y1 < y2"
   22.11    unfolding prod_le_def prod_less_def by simp_all
   22.12  
   22.13  instance prod :: (preorder, preorder) preorder proof
    23.1 --- a/src/HOL/Library/RBT.thy	Fri Aug 27 22:30:25 2010 +0200
    23.2 +++ b/src/HOL/Library/RBT.thy	Sat Aug 28 11:42:33 2010 +0200
    23.3 @@ -222,12 +222,14 @@
    23.4    "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    23.5    by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
    23.6  
    23.7 -lemma [code, code del]:
    23.8 -  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
    23.9 +lemma equal_Mapping [code]:
   23.10 +  "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
   23.11 +  by (simp add: equal Mapping_def entries_lookup)
   23.12  
   23.13 -lemma eq_Mapping [code]:
   23.14 -  "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
   23.15 -  by (simp add: eq Mapping_def entries_lookup)
   23.16 +lemma [code nbe]:
   23.17 +  "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
   23.18 +  by (fact equal_refl)
   23.19 +
   23.20  
   23.21  hide_const (open) impl_of lookup empty insert delete
   23.22    entries keys bulkload map_entry map fold
    24.1 --- a/src/HOL/List.thy	Fri Aug 27 22:30:25 2010 +0200
    24.2 +++ b/src/HOL/List.thy	Sat Aug 28 11:42:33 2010 +0200
    24.3 @@ -4721,8 +4721,8 @@
    24.4    by (simp add: null_def)
    24.5  
    24.6  lemma equal_Nil_null [code_unfold]:
    24.7 -  "eq_class.eq xs [] \<longleftrightarrow> null xs"
    24.8 -  by (simp add: eq eq_Nil_null)
    24.9 +  "HOL.equal xs [] \<longleftrightarrow> null xs"
   24.10 +  by (simp add: equal eq_Nil_null)
   24.11  
   24.12  definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
   24.13    [code_post]: "maps f xs = concat (map f xs)"
   24.14 @@ -4821,10 +4821,10 @@
   24.15    (Haskell "[]")
   24.16    (Scala "!Nil")
   24.17  
   24.18 -code_instance list :: eq
   24.19 +code_instance list :: equal
   24.20    (Haskell -)
   24.21  
   24.22 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   24.23 +code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   24.24    (Haskell infixl 4 "==")
   24.25  
   24.26  code_reserved SML
    25.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Aug 27 22:30:25 2010 +0200
    25.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Aug 28 11:42:33 2010 +0200
    25.3 @@ -202,7 +202,7 @@
    25.4    (@{const_name "top_fun_inst.top_fun"}, "'a"),
    25.5    (@{const_name "Pure.term"}, "'a"),
    25.6    (@{const_name "top_class.top"}, "'a"),
    25.7 -  (@{const_name "eq_class.eq"}, "'a"),
    25.8 +  (@{const_name "HOL.equal"}, "'a"),
    25.9    (@{const_name "Quotient.Quot_True"}, "'a")(*,
   25.10    (@{const_name "uminus"}, "'a"),
   25.11    (@{const_name "Nat.size"}, "'a"),
   25.12 @@ -237,7 +237,7 @@
   25.13   @{const_name "top_fun_inst.top_fun"},
   25.14   @{const_name "Pure.term"},
   25.15   @{const_name "top_class.top"},
   25.16 - @{const_name "eq_class.eq"},
   25.17 + @{const_name "HOL.equal"},
   25.18   @{const_name "Quotient.Quot_True"}]
   25.19  
   25.20  fun is_forbidden_mutant t =
    26.1 --- a/src/HOL/Option.thy	Fri Aug 27 22:30:25 2010 +0200
    26.2 +++ b/src/HOL/Option.thy	Sat Aug 28 11:42:33 2010 +0200
    26.3 @@ -99,8 +99,8 @@
    26.4    by (simp add: is_none_def)
    26.5  
    26.6  lemma [code_unfold]:
    26.7 -  "eq_class.eq x None \<longleftrightarrow> is_none x"
    26.8 -  by (simp add: eq is_none_none)
    26.9 +  "HOL.equal x None \<longleftrightarrow> is_none x"
   26.10 +  by (simp add: equal is_none_none)
   26.11  
   26.12  hide_const (open) is_none
   26.13  
   26.14 @@ -116,10 +116,10 @@
   26.15    (Haskell "Nothing" and "Just")
   26.16    (Scala "!None" and "Some")
   26.17  
   26.18 -code_instance option :: eq
   26.19 +code_instance option :: equal
   26.20    (Haskell -)
   26.21  
   26.22 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   26.23 +code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   26.24    (Haskell infixl 4 "==")
   26.25  
   26.26  code_reserved SML
    27.1 --- a/src/HOL/Predicate.thy	Fri Aug 27 22:30:25 2010 +0200
    27.2 +++ b/src/HOL/Predicate.thy	Sat Aug 28 11:42:33 2010 +0200
    27.3 @@ -808,8 +808,12 @@
    27.4  
    27.5  lemma eq_pred_code [code]:
    27.6    fixes P Q :: "'a pred"
    27.7 -  shows "eq_class.eq P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
    27.8 -  unfolding eq by auto
    27.9 +  shows "HOL.equal P Q \<longleftrightarrow> P \<le> Q \<and> Q \<le> P"
   27.10 +  by (auto simp add: equal)
   27.11 +
   27.12 +lemma [code nbe]:
   27.13 +  "HOL.equal (x :: 'a pred) x \<longleftrightarrow> True"
   27.14 +  by (fact equal_refl)
   27.15  
   27.16  lemma [code]:
   27.17    "pred_case f P = f (eval P)"
    28.1 --- a/src/HOL/Product_Type.thy	Fri Aug 27 22:30:25 2010 +0200
    28.2 +++ b/src/HOL/Product_Type.thy	Sat Aug 28 11:42:33 2010 +0200
    28.3 @@ -21,17 +21,17 @@
    28.4    -- "prefer plain propositional version"
    28.5  
    28.6  lemma
    28.7 -  shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
    28.8 -    and [code]: "eq_class.eq True P \<longleftrightarrow> P" 
    28.9 -    and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
   28.10 -    and [code]: "eq_class.eq P True \<longleftrightarrow> P"
   28.11 -    and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
   28.12 -  by (simp_all add: eq)
   28.13 +  shows [code]: "HOL.equal False P \<longleftrightarrow> \<not> P"
   28.14 +    and [code]: "HOL.equal True P \<longleftrightarrow> P" 
   28.15 +    and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" 
   28.16 +    and [code]: "HOL.equal P True \<longleftrightarrow> P"
   28.17 +    and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
   28.18 +  by (simp_all add: equal)
   28.19  
   28.20 -code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   28.21 +code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   28.22    (Haskell infixl 4 "==")
   28.23  
   28.24 -code_instance bool :: eq
   28.25 +code_instance bool :: equal
   28.26    (Haskell -)
   28.27  
   28.28  
   28.29 @@ -92,7 +92,7 @@
   28.30  end
   28.31  
   28.32  lemma [code]:
   28.33 -  "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
   28.34 +  "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
   28.35  
   28.36  code_type unit
   28.37    (SML "unit")
   28.38 @@ -106,10 +106,10 @@
   28.39    (Haskell "()")
   28.40    (Scala "()")
   28.41  
   28.42 -code_instance unit :: eq
   28.43 +code_instance unit :: equal
   28.44    (Haskell -)
   28.45  
   28.46 -code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   28.47 +code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   28.48    (Haskell infixl 4 "==")
   28.49  
   28.50  code_reserved SML
   28.51 @@ -277,10 +277,10 @@
   28.52    (Haskell "!((_),/ (_))")
   28.53    (Scala "!((_),/ (_))")
   28.54  
   28.55 -code_instance prod :: eq
   28.56 +code_instance prod :: equal
   28.57    (Haskell -)
   28.58  
   28.59 -code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   28.60 +code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   28.61    (Haskell infixl 4 "==")
   28.62  
   28.63  types_code
    29.1 --- a/src/HOL/Quickcheck.thy	Fri Aug 27 22:30:25 2010 +0200
    29.2 +++ b/src/HOL/Quickcheck.thy	Sat Aug 28 11:42:33 2010 +0200
    29.3 @@ -97,7 +97,7 @@
    29.4    \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    29.5    "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
    29.6  
    29.7 -instantiation "fun" :: ("{eq, term_of}", random) random
    29.8 +instantiation "fun" :: ("{equal, term_of}", random) random
    29.9  begin
   29.10  
   29.11  definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    30.1 --- a/src/HOL/Rat.thy	Fri Aug 27 22:30:25 2010 +0200
    30.2 +++ b/src/HOL/Rat.thy	Sat Aug 28 11:42:33 2010 +0200
    30.3 @@ -1083,18 +1083,18 @@
    30.4    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
    30.5  qed
    30.6  
    30.7 -instantiation rat :: eq
    30.8 +instantiation rat :: equal
    30.9  begin
   30.10  
   30.11  definition [code]:
   30.12 -  "eq_class.eq a b \<longleftrightarrow> quotient_of a = quotient_of b"
   30.13 +  "HOL.equal a b \<longleftrightarrow> quotient_of a = quotient_of b"
   30.14  
   30.15  instance proof
   30.16 -qed (simp add: eq_rat_def quotient_of_inject_eq)
   30.17 +qed (simp add: equal_rat_def quotient_of_inject_eq)
   30.18  
   30.19  lemma rat_eq_refl [code nbe]:
   30.20 -  "eq_class.eq (r::rat) r \<longleftrightarrow> True"
   30.21 -  by (rule HOL.eq_refl)
   30.22 +  "HOL.equal (r::rat) r \<longleftrightarrow> True"
   30.23 +  by (rule equal_refl)
   30.24  
   30.25  end
   30.26  
    31.1 --- a/src/HOL/RealDef.thy	Fri Aug 27 22:30:25 2010 +0200
    31.2 +++ b/src/HOL/RealDef.thy	Sat Aug 28 11:42:33 2010 +0200
    31.3 @@ -1697,19 +1697,21 @@
    31.4    "Ratreal (number_of r / number_of s) = number_of r / number_of s"
    31.5  unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
    31.6  
    31.7 -instantiation real :: eq
    31.8 +instantiation real :: equal
    31.9  begin
   31.10  
   31.11 -definition "eq_class.eq (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
   31.12 +definition "HOL.equal (x\<Colon>real) y \<longleftrightarrow> x - y = 0"
   31.13  
   31.14 -instance by default (simp add: eq_real_def)
   31.15 +instance proof
   31.16 +qed (simp add: equal_real_def)
   31.17  
   31.18 -lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq x y"
   31.19 -  by (simp add: eq_real_def eq)
   31.20 +lemma real_equal_code [code]:
   31.21 +  "HOL.equal (Ratreal x) (Ratreal y) \<longleftrightarrow> HOL.equal x y"
   31.22 +  by (simp add: equal_real_def equal)
   31.23  
   31.24 -lemma real_eq_refl [code nbe]:
   31.25 -  "eq_class.eq (x::real) x \<longleftrightarrow> True"
   31.26 -  by (rule HOL.eq_refl)
   31.27 +lemma [code nbe]:
   31.28 +  "HOL.equal (x::real) x \<longleftrightarrow> True"
   31.29 +  by (rule equal_refl)
   31.30  
   31.31  end
   31.32  
    32.1 --- a/src/HOL/String.thy	Fri Aug 27 22:30:25 2010 +0200
    32.2 +++ b/src/HOL/String.thy	Sat Aug 28 11:42:33 2010 +0200
    32.3 @@ -183,10 +183,10 @@
    32.4    fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
    32.5  *}
    32.6  
    32.7 -code_instance literal :: eq
    32.8 +code_instance literal :: equal
    32.9    (Haskell -)
   32.10  
   32.11 -code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   32.12 +code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   32.13    (SML "!((_ : string) = _)")
   32.14    (OCaml "!((_ : string) = _)")
   32.15    (Haskell infixl 4 "==")
    33.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Aug 27 22:30:25 2010 +0200
    33.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Aug 28 11:42:33 2010 +0200
    33.3 @@ -68,7 +68,7 @@
    33.4      val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
    33.5        Datatype_Data.the_info thy tyco;
    33.6      val ty = Type (tyco, map TFree vs);
    33.7 -    fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
    33.8 +    fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT)
    33.9        $ t1 $ t2;
   33.10      fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
   33.11      fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
   33.12 @@ -83,7 +83,7 @@
   33.13      val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
   33.14      val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
   33.15      val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps 
   33.16 -      (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
   33.17 +      (map Simpdata.mk_eq (@{thm equal} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
   33.18      fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
   33.19        |> Simpdata.mk_eq;
   33.20    in (map prove (triv_injects @ injects @ distincts), prove refl) end;
   33.21 @@ -96,7 +96,7 @@
   33.22          fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
   33.23            $ Free ("x", ty) $ Free ("y", ty);
   33.24          val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
   33.25 -          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
   33.26 +          (mk_side @{const_name HOL.equal}, mk_side @{const_name "op ="}));
   33.27          val def' = Syntax.check_term lthy def;
   33.28          val ((_, (_, thm)), lthy') = Specification.definition
   33.29            (NONE, (Attrib.empty_binding, def')) lthy;
   33.30 @@ -115,7 +115,7 @@
   33.31        #> snd
   33.32    in
   33.33      thy
   33.34 -    |> Class.instantiation (tycos, vs, [HOLogic.class_eq])
   33.35 +    |> Class.instantiation (tycos, vs, [HOLogic.class_equal])
   33.36      |> fold_map add_def tycos
   33.37      |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
   33.38           (fn _ => fn def_thms => tac def_thms) def_thms)
   33.39 @@ -135,7 +135,7 @@
   33.40      val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos;
   33.41      val certs = map (mk_case_cert thy) tycos;
   33.42      val tycos_eq = filter_out
   33.43 -      (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_eq]) tycos;
   33.44 +      (fn tyco => can (Sorts.mg_domain (Sign.classes_of thy) tyco) [HOLogic.class_equal]) tycos;
   33.45    in
   33.46      if null css then thy
   33.47      else thy
    34.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Aug 27 22:30:25 2010 +0200
    34.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Aug 28 11:42:33 2010 +0200
    34.3 @@ -182,7 +182,7 @@
    34.4  fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
    34.5  
    34.6  val syntactic_sorts =
    34.7 -  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
    34.8 +  @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
    34.9    @{sort number}
   34.10  fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
   34.11      subset (op =) (S, syntactic_sorts)
    35.1 --- a/src/HOL/Tools/hologic.ML	Fri Aug 27 22:30:25 2010 +0200
    35.2 +++ b/src/HOL/Tools/hologic.ML	Sat Aug 28 11:42:33 2010 +0200
    35.3 @@ -49,7 +49,7 @@
    35.4    val exists_const: typ -> term
    35.5    val mk_exists: string * typ * term -> term
    35.6    val choice_const: typ -> term
    35.7 -  val class_eq: string
    35.8 +  val class_equal: string
    35.9    val mk_binop: string -> term * term -> term
   35.10    val mk_binrel: string -> term * term -> term
   35.11    val dest_bin: string -> typ -> term -> term * term
   35.12 @@ -251,7 +251,7 @@
   35.13  
   35.14  fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
   35.15  
   35.16 -val class_eq = "HOL.eq";
   35.17 +val class_equal = "HOL.equal";
   35.18  
   35.19  
   35.20  (* binary operations and relations *)
    36.1 --- a/src/HOL/Tools/record.ML	Fri Aug 27 22:30:25 2010 +0200
    36.2 +++ b/src/HOL/Tools/record.ML	Sat Aug 28 11:42:33 2010 +0200
    36.3 @@ -1844,7 +1844,7 @@
    36.4    let
    36.5      val eq =
    36.6        (HOLogic.mk_Trueprop o HOLogic.mk_eq)
    36.7 -        (Const (@{const_name eq_class.eq}, extT --> extT --> HOLogic.boolT),
    36.8 +        (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
    36.9           Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
   36.10      fun tac eq_def =
   36.11        Class.intro_classes_tac []
   36.12 @@ -1853,15 +1853,15 @@
   36.13      fun mk_eq thy eq_def = Simplifier.rewrite_rule
   36.14        [(AxClass.unoverload thy o Thm.symmetric o Simpdata.mk_eq) eq_def] inject;
   36.15      fun mk_eq_refl thy =
   36.16 -      @{thm HOL.eq_refl}
   36.17 +      @{thm equal_refl}
   36.18        |> Thm.instantiate
   36.19 -        ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global extT)], [])
   36.20 +        ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
   36.21        |> AxClass.unoverload thy;
   36.22    in
   36.23      thy
   36.24      |> Code.add_datatype [ext]
   36.25      |> fold Code.add_default_eqn simps
   36.26 -    |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_eq])
   36.27 +    |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
   36.28      |> `(fn lthy => Syntax.check_term lthy eq)
   36.29      |-> (fn eq => Specification.definition
   36.30           (NONE, (Attrib.empty_binding, eq)))
    37.1 --- a/src/HOL/Typerep.thy	Fri Aug 27 22:30:25 2010 +0200
    37.2 +++ b/src/HOL/Typerep.thy	Sat Aug 28 11:42:33 2010 +0200
    37.3 @@ -78,9 +78,13 @@
    37.4  *}
    37.5  
    37.6  lemma [code]:
    37.7 -  "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
    37.8 -     \<and> list_all2 eq_class.eq tys1 tys2"
    37.9 -  by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
   37.10 +  "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
   37.11 +     \<and> list_all2 HOL.equal tys1 tys2"
   37.12 +  by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
   37.13 +
   37.14 +lemma [code nbe]:
   37.15 +  "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
   37.16 +  by (fact equal_refl)
   37.17  
   37.18  code_type typerep
   37.19    (Eval "Term.typ")
    38.1 --- a/src/HOL/Word/Word.thy	Fri Aug 27 22:30:25 2010 +0200
    38.2 +++ b/src/HOL/Word/Word.thy	Sat Aug 28 11:42:33 2010 +0200
    38.3 @@ -953,14 +953,14 @@
    38.4  
    38.5  text {* Executable equality *}
    38.6  
    38.7 -instantiation word :: ("{len0}") eq
    38.8 +instantiation word :: (len0) equal
    38.9  begin
   38.10  
   38.11 -definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
   38.12 -  "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
   38.13 +definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
   38.14 +  "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
   38.15  
   38.16  instance proof
   38.17 -qed (simp add: eq eq_word_def)
   38.18 +qed (simp add: equal equal_word_def)
   38.19  
   38.20  end
   38.21  
    39.1 --- a/src/HOL/ex/Numeral.thy	Fri Aug 27 22:30:25 2010 +0200
    39.2 +++ b/src/HOL/ex/Numeral.thy	Sat Aug 28 11:42:33 2010 +0200
    39.3 @@ -845,7 +845,7 @@
    39.4    "(uminus :: int \<Rightarrow> int) = uminus"
    39.5    "(op - :: int \<Rightarrow> int \<Rightarrow> int) = op -"
    39.6    "(op * :: int \<Rightarrow> int \<Rightarrow> int) = op *"
    39.7 -  "(eq_class.eq :: int \<Rightarrow> int \<Rightarrow> bool) = eq_class.eq"
    39.8 +  "(HOL.equal :: int \<Rightarrow> int \<Rightarrow> bool) = HOL.equal"
    39.9    "(op \<le> :: int \<Rightarrow> int \<Rightarrow> bool) = op \<le>"
   39.10    "(op < :: int \<Rightarrow> int \<Rightarrow> bool) = op <"
   39.11    by rule+
   39.12 @@ -928,16 +928,20 @@
   39.13    by simp_all
   39.14  
   39.15  lemma eq_int_code [code]:
   39.16 -  "eq_class.eq 0 (0::int) \<longleftrightarrow> True"
   39.17 -  "eq_class.eq 0 (Pls l) \<longleftrightarrow> False"
   39.18 -  "eq_class.eq 0 (Mns l) \<longleftrightarrow> False"
   39.19 -  "eq_class.eq (Pls k) 0 \<longleftrightarrow> False"
   39.20 -  "eq_class.eq (Pls k) (Pls l) \<longleftrightarrow> eq_class.eq k l"
   39.21 -  "eq_class.eq (Pls k) (Mns l) \<longleftrightarrow> False"
   39.22 -  "eq_class.eq (Mns k) 0 \<longleftrightarrow> False"
   39.23 -  "eq_class.eq (Mns k) (Pls l) \<longleftrightarrow> False"
   39.24 -  "eq_class.eq (Mns k) (Mns l) \<longleftrightarrow> eq_class.eq k l"
   39.25 -  by (auto simp add: eq dest: sym)
   39.26 +  "HOL.equal 0 (0::int) \<longleftrightarrow> True"
   39.27 +  "HOL.equal 0 (Pls l) \<longleftrightarrow> False"
   39.28 +  "HOL.equal 0 (Mns l) \<longleftrightarrow> False"
   39.29 +  "HOL.equal (Pls k) 0 \<longleftrightarrow> False"
   39.30 +  "HOL.equal (Pls k) (Pls l) \<longleftrightarrow> HOL.equal k l"
   39.31 +  "HOL.equal (Pls k) (Mns l) \<longleftrightarrow> False"
   39.32 +  "HOL.equal (Mns k) 0 \<longleftrightarrow> False"
   39.33 +  "HOL.equal (Mns k) (Pls l) \<longleftrightarrow> False"
   39.34 +  "HOL.equal (Mns k) (Mns l) \<longleftrightarrow> HOL.equal k l"
   39.35 +  by (auto simp add: equal dest: sym)
   39.36 +
   39.37 +lemma [code nbe]:
   39.38 +  "HOL.equal (k::int) k \<longleftrightarrow> True"
   39.39 +  by (fact equal_refl)
   39.40  
   39.41  lemma less_eq_int_code [code]:
   39.42    "0 \<le> (0::int) \<longleftrightarrow> True"
   39.43 @@ -1078,7 +1082,7 @@
   39.44    (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   39.45    (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
   39.46  
   39.47 -code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   39.48 +code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   39.49    (SML "!((_ : IntInf.int) = _)")
   39.50    (OCaml "Big'_int.eq'_big'_int")
   39.51    (Haskell infixl 4 "==")
    40.1 --- a/src/Tools/Code/code_scala.ML	Fri Aug 27 22:30:25 2010 +0200
    40.2 +++ b/src/Tools/Code/code_scala.ML	Sat Aug 28 11:42:33 2010 +0200
    40.3 @@ -444,18 +444,15 @@
    40.4        (make_vars reserved) args_num is_singleton_constr;
    40.5  
    40.6      (* print nodes *)
    40.7 +    fun print_module base implicit_ps p = Pretty.chunks2
    40.8 +      ([str ("object " ^ base ^ " {")]
    40.9 +        @ (if null implicit_ps then [] else (single o Pretty.block)
   40.10 +            (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
   40.11 +        @ [p, str ("} /* object " ^ base ^ " */")]);
   40.12      fun print_implicit prefix_fragments implicit =
   40.13        let
   40.14          val s = deresolver prefix_fragments implicit;
   40.15        in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
   40.16 -    fun print_implicits prefix_fragments implicits =
   40.17 -      case map_filter (print_implicit prefix_fragments) implicits
   40.18 -       of [] => NONE
   40.19 -        | ps => (SOME o Pretty.block)
   40.20 -            (str "import /*implicits*/" :: Pretty.brk 1 :: commas ps);
   40.21 -    fun print_module prefix_fragments base implicits p = Pretty.chunks2
   40.22 -      ([str ("object " ^ base ^ " {")] @ the_list (print_implicits prefix_fragments implicits)
   40.23 -        @ [p, str ("} /* object " ^ base ^ " */")]);
   40.24      fun print_node _ (_, Dummy) = NONE
   40.25        | print_node prefix_fragments (name, Stmt stmt) =
   40.26            if null presentation_stmt_names
   40.27 @@ -464,10 +461,14 @@
   40.28            else NONE
   40.29        | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
   40.30            if null presentation_stmt_names
   40.31 -          then case print_nodes (prefix_fragments @ [name_fragment]) nodes
   40.32 -           of NONE => NONE
   40.33 -            | SOME p => SOME (print_module prefix_fragments
   40.34 -                (Long_Name.base_name name_fragment) implicits p)
   40.35 +          then
   40.36 +            let
   40.37 +              val prefix_fragments' = prefix_fragments @ [name_fragment];
   40.38 +            in
   40.39 +              Option.map (print_module name_fragment
   40.40 +                (map_filter (print_implicit prefix_fragments') implicits))
   40.41 +                  (print_nodes prefix_fragments' nodes)
   40.42 +            end
   40.43            else print_nodes [] nodes
   40.44      and print_nodes prefix_fragments nodes = let
   40.45          val ps = map_filter (fn name => print_node prefix_fragments (name,
   40.46 @@ -477,7 +478,7 @@
   40.47  
   40.48      (* serialization *)
   40.49      val p_includes = if null presentation_stmt_names
   40.50 -      then map (fn (base, p) => print_module [] base [] p) includes else [];
   40.51 +      then map (fn (base, p) => print_module base [] p) includes else [];
   40.52      val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   40.53    in
   40.54      Code_Target.mk_serialization target