src/HOL/Relation.thy
changeset 55096 916b2ac758f4
parent 55083 0a689157e3ce
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Relation.thy	Tue Jan 21 13:05:22 2014 +0100
     1.2 +++ b/src/HOL/Relation.thy	Tue Jan 21 13:21:55 2014 +0100
     1.3 @@ -930,12 +930,6 @@
     1.4    "Domain r = {x. \<exists>y. (x, y) \<in> r}"
     1.5    by blast
     1.6  
     1.7 -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
     1.8 -  by auto
     1.9 -
    1.10 -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
    1.11 -  by auto
    1.12 -
    1.13  
    1.14  subsubsection {* Image of a set under a relation *}
    1.15