| changeset 58157 | c376c43c346c |
| parent 57514 | bdc2c6b40bf2 |
| child 58410 | 6d46ad54a2ab |
--- 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]: