--- 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