# HG changeset patch
# User blanchet
# Date 1409695590 -7200
# Node ID c376c43c346cc9025224b7b7166b095139e8e342
# Parent  e333bd3b4d3d34c18f54b54c99b28f6f3deff711
moved old datatype material around

diff -r e333bd3b4d3d -r c376c43c346c src/HOL/Old_Datatype.thy
--- 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
diff -r e333bd3b4d3d -r c376c43c346c src/HOL/Power.thy
--- 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]: