src/HOL/Datatype.thy
changeset 29609 a010aab5bed0
parent 29580 117b88da143c
child 30235 58d147683393
     1.1 --- a/src/HOL/Datatype.thy	Wed Jan 21 23:40:23 2009 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Nat Relation
     1.8 +imports Nat Product_Type
     1.9  begin
    1.10  
    1.11  typedef (Node)
    1.12 @@ -509,15 +509,6 @@
    1.13  lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
    1.14  
    1.15  
    1.16 -(*** Domain ***)
    1.17 -
    1.18 -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
    1.19 -by auto
    1.20 -
    1.21 -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
    1.22 -by auto
    1.23 -
    1.24 -
    1.25  text {* hides popular names *}
    1.26  hide (open) type node item
    1.27  hide (open) const Push Node Atom Leaf Numb Lim Split Case