dropped eq const
authorhaftmann
Wed Nov 22 10:20:12 2006 +0100 (2006-11-22)
changeset 21454a1937c51ed88
parent 21453 03ca07d478be
child 21455 b6be1d1b66c5
dropped eq const
src/HOL/Code_Generator.thy
src/HOL/Datatype.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/Presburger.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Presburger.thy
src/HOL/Product_Type.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/datatype_codegen.ML
     1.1 --- a/src/HOL/Code_Generator.thy	Wed Nov 22 10:20:11 2006 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Wed Nov 22 10:20:12 2006 +0100
     1.3 @@ -192,13 +192,8 @@
     1.4  
     1.5  subsubsection {* eq class *}
     1.6  
     1.7 -class eq =
     1.8 -  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.9 -
    1.10 -defs
    1.11 -  eq_def [normal post]: "eq \<equiv> (op =)"
    1.12 -
    1.13 -lemmas [symmetric, code inline, code func] = eq_def
    1.14 +axclass eq \<subseteq> type
    1.15 +  attach "op ="
    1.16  
    1.17  
    1.18  subsubsection {* bool type *}
    1.19 @@ -206,36 +201,36 @@
    1.20  instance bool :: eq ..
    1.21  
    1.22  lemma [code func]:
    1.23 -  "eq True p = p" unfolding eq_def by auto
    1.24 +  "True = P \<longleftrightarrow> P" by simp
    1.25  
    1.26  lemma [code func]:
    1.27 -  "eq False p = (\<not> p)" unfolding eq_def by auto
    1.28 +  "False = P \<longleftrightarrow> \<not> P" by simp
    1.29  
    1.30  lemma [code func]:
    1.31 -  "eq p True = p" unfolding eq_def by auto
    1.32 +  "P = True \<longleftrightarrow> P" by simp
    1.33  
    1.34  lemma [code func]:
    1.35 -  "eq p False = (\<not> p)" unfolding eq_def by auto
    1.36 +  "P = False \<longleftrightarrow> \<not> P" by simp
    1.37  
    1.38  
    1.39  subsubsection {* Haskell *}
    1.40  
    1.41  code_class eq
    1.42 -  (Haskell "Eq" where eq \<equiv> "(==)")
    1.43 +  (Haskell "Eq" where "op =" \<equiv> "(==)")
    1.44  
    1.45 -code_const eq
    1.46 +code_const "op ="
    1.47    (Haskell infixl 4 "==")
    1.48  
    1.49  code_instance bool :: eq
    1.50    (Haskell -)
    1.51  
    1.52 -code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.53 +code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.54    (Haskell infixl 4 "==")
    1.55  
    1.56  code_reserved Haskell
    1.57    Eq eq
    1.58  
    1.59  
    1.60 -hide (open) const eq if_delayed
    1.61 +hide (open) const if_delayed
    1.62  
    1.63  end
    1.64 \ No newline at end of file
     2.1 --- a/src/HOL/Datatype.thy	Wed Nov 22 10:20:11 2006 +0100
     2.2 +++ b/src/HOL/Datatype.thy	Wed Nov 22 10:20:12 2006 +0100
     2.3 @@ -799,7 +799,7 @@
     2.4  code_instance option :: eq
     2.5    (Haskell -)
     2.6  
     2.7 -code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
     2.8 +code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
     2.9    (Haskell infixl 4 "==")
    2.10  
    2.11  code_reserved SML
     3.1 --- a/src/HOL/Integ/IntDef.thy	Wed Nov 22 10:20:11 2006 +0100
     3.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Nov 22 10:20:12 2006 +0100
     3.3 @@ -917,7 +917,7 @@
     3.4  code_instance int :: eq
     3.5    (Haskell -)
     3.6  
     3.7 -code_const "Code_Generator.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     3.8 +code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     3.9    (SML "!((_ : IntInf.int) = _)")
    3.10    (Haskell infixl 4 "==")
    3.11  
     4.1 --- a/src/HOL/Integ/Presburger.thy	Wed Nov 22 10:20:11 2006 +0100
     4.2 +++ b/src/HOL/Integ/Presburger.thy	Wed Nov 22 10:20:12 2006 +0100
     4.3 @@ -1090,12 +1090,12 @@
     4.4  text {* Code generator setup *}
     4.5  
     4.6  text {*
     4.7 -  Presburger arithmetic is neccesary to prove some
     4.8 +  Presburger arithmetic is necessary (at least convenient) to prove some
     4.9    of the following code lemmas on integer numerals.
    4.10  *}
    4.11  
    4.12  lemma eq_number_of [code func]:
    4.13 -  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
    4.14 +  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    4.15    unfolding number_of_is_id ..
    4.16  
    4.17  lemma less_eq_number_of [code func]:
    4.18 @@ -1103,57 +1103,55 @@
    4.19    unfolding number_of_is_id ..
    4.20  
    4.21  lemma eq_Pls_Pls:
    4.22 -  "Code_Generator.eq Numeral.Pls Numeral.Pls"
    4.23 -  unfolding eq_def ..
    4.24 +  "Numeral.Pls = Numeral.Pls" ..
    4.25  
    4.26  lemma eq_Pls_Min:
    4.27 -  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
    4.28 -  unfolding eq_def Pls_def Min_def by auto
    4.29 +  "Numeral.Pls \<noteq> Numeral.Min"
    4.30 +  unfolding Pls_def Min_def by auto
    4.31  
    4.32  lemma eq_Pls_Bit0:
    4.33 -  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    4.34 -  unfolding eq_def Pls_def Bit_def bit.cases by auto
    4.35 +  "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
    4.36 +  unfolding Pls_def Bit_def bit.cases by auto
    4.37  
    4.38  lemma eq_Pls_Bit1:
    4.39 -  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    4.40 -  unfolding eq_def Pls_def Bit_def bit.cases by arith
    4.41 +  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
    4.42 +  unfolding Pls_def Bit_def bit.cases by arith
    4.43  
    4.44  lemma eq_Min_Pls:
    4.45 -  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
    4.46 -  unfolding eq_def Pls_def Min_def by auto
    4.47 +  "Numeral.Min \<noteq> Numeral.Pls"
    4.48 +  unfolding Pls_def Min_def by auto
    4.49  
    4.50  lemma eq_Min_Min:
    4.51 -  "Code_Generator.eq Numeral.Min Numeral.Min"
    4.52 -  unfolding eq_def ..
    4.53 +  "Numeral.Min = Numeral.Min" ..
    4.54  
    4.55  lemma eq_Min_Bit0:
    4.56 -  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
    4.57 -  unfolding eq_def Min_def Bit_def bit.cases by arith
    4.58 +  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
    4.59 +  unfolding Min_def Bit_def bit.cases by arith
    4.60  
    4.61  lemma eq_Min_Bit1:
    4.62 -  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    4.63 -  unfolding eq_def Min_def Bit_def bit.cases by auto
    4.64 +  "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
    4.65 +  unfolding Min_def Bit_def bit.cases by auto
    4.66  
    4.67  lemma eq_Bit0_Pls:
    4.68 -  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    4.69 -  unfolding eq_def Pls_def Bit_def bit.cases by auto
    4.70 +  "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
    4.71 +  unfolding Pls_def Bit_def bit.cases by auto
    4.72  
    4.73  lemma eq_Bit1_Pls:
    4.74 -  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    4.75 -  unfolding eq_def Pls_def Bit_def bit.cases by arith
    4.76 +  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
    4.77 +  unfolding Pls_def Bit_def bit.cases by arith
    4.78  
    4.79  lemma eq_Bit0_Min:
    4.80 -  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
    4.81 -  unfolding eq_def Min_def Bit_def bit.cases by arith
    4.82 +  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
    4.83 +  unfolding Min_def Bit_def bit.cases by arith
    4.84  
    4.85  lemma eq_Bit1_Min:
    4.86 -  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    4.87 -  unfolding eq_def Min_def Bit_def bit.cases by auto
    4.88 +  "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
    4.89 +  unfolding Min_def Bit_def bit.cases by auto
    4.90  
    4.91  lemma eq_Bit_Bit:
    4.92 -  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    4.93 -    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
    4.94 -  unfolding eq_def Bit_def
    4.95 +  "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
    4.96 +    v1 = v2 \<and> k1 = k2"
    4.97 +  unfolding Bit_def
    4.98    apply (cases v1)
    4.99    apply (cases v2)
   4.100    apply auto
     5.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Nov 22 10:20:11 2006 +0100
     5.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Nov 22 10:20:12 2006 +0100
     5.3 @@ -50,8 +50,8 @@
     5.4  qed
     5.5  
     5.6  lemma [code inline]:
     5.7 -  "nat_case f g n = (if Code_Generator.eq n 0 then f else g (nat_of_int (int n - 1)))"
     5.8 -  by (cases n) (simp_all add: eq_def nat_of_int_int)
     5.9 +  "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
    5.10 +  by (cases n) (simp_all add: nat_of_int_int)
    5.11  
    5.12  text {*
    5.13    Most standard arithmetic functions on natural numbers are implemented
    5.14 @@ -97,8 +97,8 @@
    5.15    by simp
    5.16  lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
    5.17    by simp
    5.18 -lemma [code func, code inline]: "Code_Generator.eq m n \<longleftrightarrow> Code_Generator.eq (int m) (int n)"
    5.19 -  unfolding eq_def by simp
    5.20 +lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
    5.21 +  by simp
    5.22  lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
    5.23  proof (cases "k < 0")
    5.24    case True then show ?thesis by simp
     6.1 --- a/src/HOL/Library/ExecutableRat.thy	Wed Nov 22 10:20:11 2006 +0100
     6.2 +++ b/src/HOL/Library/ExecutableRat.thy	Wed Nov 22 10:20:12 2006 +0100
     6.3 @@ -121,7 +121,7 @@
     6.4    "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
     6.5    "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
     6.6    "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
     6.7 -  "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
     6.8 +  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
     6.9  
    6.10  code_const div_zero
    6.11    (SML "raise/ (Fail/ \"Division by zero\")")
    6.12 @@ -136,7 +136,7 @@
    6.13    "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
    6.14    "inverse \<Colon> rat \<Rightarrow> rat"
    6.15    "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
    6.16 -   "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
    6.17 +  "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
    6.18    (SML *)
    6.19  
    6.20  
     7.1 --- a/src/HOL/Library/ExecutableSet.thy	Wed Nov 22 10:20:11 2006 +0100
     7.2 +++ b/src/HOL/Library/ExecutableSet.thy	Wed Nov 22 10:20:12 2006 +0100
     7.3 @@ -32,10 +32,6 @@
     7.4    by blast
     7.5  
     7.6  lemma [code func]:
     7.7 -  "Code_Generator.eq A B \<longleftrightarrow> subset A B \<and> subset B A"
     7.8 -  unfolding eq_def subset_def by blast
     7.9 -
    7.10 -lemma [code func]:
    7.11    "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    7.12    unfolding subset_def Set.subset_def ..
    7.13  
     8.1 --- a/src/HOL/Presburger.thy	Wed Nov 22 10:20:11 2006 +0100
     8.2 +++ b/src/HOL/Presburger.thy	Wed Nov 22 10:20:12 2006 +0100
     8.3 @@ -1090,12 +1090,12 @@
     8.4  text {* Code generator setup *}
     8.5  
     8.6  text {*
     8.7 -  Presburger arithmetic is neccesary to prove some
     8.8 +  Presburger arithmetic is necessary (at least convenient) to prove some
     8.9    of the following code lemmas on integer numerals.
    8.10  *}
    8.11  
    8.12  lemma eq_number_of [code func]:
    8.13 -  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
    8.14 +  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    8.15    unfolding number_of_is_id ..
    8.16  
    8.17  lemma less_eq_number_of [code func]:
    8.18 @@ -1103,57 +1103,55 @@
    8.19    unfolding number_of_is_id ..
    8.20  
    8.21  lemma eq_Pls_Pls:
    8.22 -  "Code_Generator.eq Numeral.Pls Numeral.Pls"
    8.23 -  unfolding eq_def ..
    8.24 +  "Numeral.Pls = Numeral.Pls" ..
    8.25  
    8.26  lemma eq_Pls_Min:
    8.27 -  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
    8.28 -  unfolding eq_def Pls_def Min_def by auto
    8.29 +  "Numeral.Pls \<noteq> Numeral.Min"
    8.30 +  unfolding Pls_def Min_def by auto
    8.31  
    8.32  lemma eq_Pls_Bit0:
    8.33 -  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    8.34 -  unfolding eq_def Pls_def Bit_def bit.cases by auto
    8.35 +  "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
    8.36 +  unfolding Pls_def Bit_def bit.cases by auto
    8.37  
    8.38  lemma eq_Pls_Bit1:
    8.39 -  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    8.40 -  unfolding eq_def Pls_def Bit_def bit.cases by arith
    8.41 +  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
    8.42 +  unfolding Pls_def Bit_def bit.cases by arith
    8.43  
    8.44  lemma eq_Min_Pls:
    8.45 -  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
    8.46 -  unfolding eq_def Pls_def Min_def by auto
    8.47 +  "Numeral.Min \<noteq> Numeral.Pls"
    8.48 +  unfolding Pls_def Min_def by auto
    8.49  
    8.50  lemma eq_Min_Min:
    8.51 -  "Code_Generator.eq Numeral.Min Numeral.Min"
    8.52 -  unfolding eq_def ..
    8.53 +  "Numeral.Min = Numeral.Min" ..
    8.54  
    8.55  lemma eq_Min_Bit0:
    8.56 -  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
    8.57 -  unfolding eq_def Min_def Bit_def bit.cases by arith
    8.58 +  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
    8.59 +  unfolding Min_def Bit_def bit.cases by arith
    8.60  
    8.61  lemma eq_Min_Bit1:
    8.62 -  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    8.63 -  unfolding eq_def Min_def Bit_def bit.cases by auto
    8.64 +  "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
    8.65 +  unfolding Min_def Bit_def bit.cases by auto
    8.66  
    8.67  lemma eq_Bit0_Pls:
    8.68 -  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    8.69 -  unfolding eq_def Pls_def Bit_def bit.cases by auto
    8.70 +  "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
    8.71 +  unfolding Pls_def Bit_def bit.cases by auto
    8.72  
    8.73  lemma eq_Bit1_Pls:
    8.74 -  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    8.75 -  unfolding eq_def Pls_def Bit_def bit.cases by arith
    8.76 +  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
    8.77 +  unfolding Pls_def Bit_def bit.cases by arith
    8.78  
    8.79  lemma eq_Bit0_Min:
    8.80 -  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
    8.81 -  unfolding eq_def Min_def Bit_def bit.cases by arith
    8.82 +  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
    8.83 +  unfolding Min_def Bit_def bit.cases by arith
    8.84  
    8.85  lemma eq_Bit1_Min:
    8.86 -  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    8.87 -  unfolding eq_def Min_def Bit_def bit.cases by auto
    8.88 +  "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
    8.89 +  unfolding Min_def Bit_def bit.cases by auto
    8.90  
    8.91  lemma eq_Bit_Bit:
    8.92 -  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    8.93 -    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
    8.94 -  unfolding eq_def Bit_def
    8.95 +  "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
    8.96 +    v1 = v2 \<and> k1 = k2"
    8.97 +  unfolding Bit_def
    8.98    apply (cases v1)
    8.99    apply (cases v2)
   8.100    apply auto
     9.1 --- a/src/HOL/Product_Type.thy	Wed Nov 22 10:20:11 2006 +0100
     9.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 22 10:20:12 2006 +0100
     9.3 @@ -776,7 +776,7 @@
     9.4  instance unit :: eq ..
     9.5  
     9.6  lemma [code func]:
     9.7 -  "Code_Generator.eq (u\<Colon>unit) v = True" unfolding eq_def unit_eq [of u] unit_eq [of v] by rule+
     9.8 +  "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
     9.9  
    9.10  code_instance unit :: eq
    9.11    (Haskell -)
    9.12 @@ -784,16 +784,15 @@
    9.13  instance * :: (eq, eq) eq ..
    9.14  
    9.15  lemma [code func]:
    9.16 -  "Code_Generator.eq (x1, y1) (x2, y2) = (Code_Generator.eq x1 x2 \<and> Code_Generator.eq y1 y2)"
    9.17 -  unfolding eq_def by auto
    9.18 +  "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
    9.19  
    9.20  code_instance * :: eq
    9.21    (Haskell -)
    9.22  
    9.23 -code_const "Code_Generator.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    9.24 +code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    9.25    (Haskell infixl 4 "==")
    9.26  
    9.27 -code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    9.28 +code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    9.29    (Haskell infixl 4 "==")
    9.30  
    9.31  types_code
    10.1 --- a/src/HOL/Sum_Type.thy	Wed Nov 22 10:20:11 2006 +0100
    10.2 +++ b/src/HOL/Sum_Type.thy	Wed Nov 22 10:20:12 2006 +0100
    10.3 @@ -197,20 +197,20 @@
    10.4  instance "+" :: (eq, eq) eq ..
    10.5  
    10.6  lemma [code func]:
    10.7 -  "Code_Generator.eq (Inl x) (Inl y) = Code_Generator.eq x y"
    10.8 -  unfolding eq_def Inl_eq ..
    10.9 +  "(Inl x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inl y \<longleftrightarrow> x = y"
   10.10 +  unfolding Inl_eq ..
   10.11  
   10.12  lemma [code func]:
   10.13 -  "Code_Generator.eq (Inr x) (Inr y) = Code_Generator.eq x y"
   10.14 -  unfolding eq_def Inr_eq ..
   10.15 +  "(Inr x \<Colon> 'a\<Colon>eq + 'b\<Colon>eq) = Inr y \<longleftrightarrow> x = y"
   10.16 +  unfolding Inr_eq ..
   10.17  
   10.18  lemma [code func]:
   10.19 -  "Code_Generator.eq (Inl x) (Inr y) = False"
   10.20 -  unfolding eq_def using Inl_not_Inr by auto
   10.21 +  "Inl (x\<Colon>'a\<Colon>eq) = Inr (y\<Colon>'b\<Colon>eq) \<longleftrightarrow> False"
   10.22 +  using Inl_not_Inr by auto
   10.23  
   10.24  lemma [code func]:
   10.25 -  "Code_Generator.eq (Inr x) (Inl y) = False"
   10.26 -  unfolding eq_def using Inr_not_Inl by auto
   10.27 +  "Inr (x\<Colon>'b\<Colon>eq) = Inl (y\<Colon>'a\<Colon>eq) \<longleftrightarrow> False"
   10.28 +  using Inr_not_Inl by auto
   10.29  
   10.30  ML
   10.31  {*
    11.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Nov 22 10:20:11 2006 +0100
    11.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Nov 22 10:20:12 2006 +0100
    11.3 @@ -489,7 +489,6 @@
    11.4    | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
    11.5  
    11.6  local
    11.7 -  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
    11.8    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    11.9     of SOME _ => get_eq_datatype thy tyco
   11.10      | NONE => [TypecopyPackage.get_eq thy tyco];
   11.11 @@ -498,7 +497,6 @@
   11.12      get_eq_thms thy tyco
   11.13      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
   11.14      |> HOL.constrain_op_eq_thms thy
   11.15 -    |> map (Tactic.rewrite_rule [eq_def_sym])
   11.16  end;
   11.17  
   11.18  type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
   11.19 @@ -605,7 +603,7 @@
   11.20        let
   11.21          val thy_ref = Theory.self_ref thy;
   11.22          val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
   11.23 -        val c = CodegenConsts.norm thy ("Code_Generator.eq", [ty]);
   11.24 +        val c = CodegenConsts.norm thy ("op =", [ty]);
   11.25          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   11.26        in
   11.27          CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy