src/HOL/Power.thy
changeset 58157 c376c43c346c
parent 57514 bdc2c6b40bf2
child 58410 6d46ad54a2ab
     1.1 --- a/src/HOL/Power.thy	Wed Sep 03 00:06:28 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Wed Sep 03 00:06:30 2014 +0200
     1.3 @@ -822,12 +822,6 @@
     1.4    ultimately show ?thesis by blast
     1.5  qed
     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  subsection {* Code generator tweak *}
    1.14  
    1.15  lemma power_power_power [code]: