--- a/src/HOL/Old_Datatype.thy Wed Sep 03 00:06:28 2014 +0200
+++ b/src/HOL/Old_Datatype.thy Wed Sep 03 00:06:30 2014 +0200
@@ -6,7 +6,7 @@
header {* Old Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *}
theory Old_Datatype
-imports Product_Type Sum_Type Nat
+imports Power
keywords "datatype" :: thy_decl
begin
@@ -508,6 +508,15 @@
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
+(*** Domain theorems ***)
+
+lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
+ by auto
+
+lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
+ by auto
+
+
text {* hides popular names *}
hide_type (open) node item
hide_const (open) Push Node Atom Leaf Numb Lim Split Case
--- a/src/HOL/Power.thy Wed Sep 03 00:06:28 2014 +0200
+++ b/src/HOL/Power.thy Wed Sep 03 00:06:30 2014 +0200
@@ -822,12 +822,6 @@
ultimately show ?thesis by blast
qed
-lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
- by auto
-
-lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
- by auto
-
subsection {* Code generator tweak *}
lemma power_power_power [code]: