src/HOL/Product_Type.thy
changeset 33275 b497b2574bf6
parent 33271 7be66dee1a5a
child 33594 357f74e0090c
     1.1 --- a/src/HOL/Product_Type.thy	Wed Oct 28 17:44:03 2009 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 28 17:44:03 2009 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Cartesian products *}
     1.5  
     1.6  theory Product_Type
     1.7 -imports Inductive Nat
     1.8 +imports Inductive
     1.9  uses
    1.10    ("Tools/split_rule.ML")
    1.11    ("Tools/inductive_set.ML")
    1.12 @@ -94,8 +94,6 @@
    1.13  
    1.14  text {* code generator setup *}
    1.15  
    1.16 -instance unit :: eq ..
    1.17 -
    1.18  lemma [code]:
    1.19    "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
    1.20  
    1.21 @@ -932,8 +930,6 @@
    1.22  
    1.23  subsubsection {* Code generator setup *}
    1.24  
    1.25 -instance * :: (eq, eq) eq ..
    1.26 -
    1.27  lemma [code]:
    1.28    "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
    1.29