| changeset 47225 | 650318981557 |
| parent 47224 | 773fe2754b8c |
| child 54227 | 63b441f49645 |
--- a/src/HOL/Parity.thy Fri Mar 30 15:24:24 2012 +0200 +++ b/src/HOL/Parity.thy Fri Mar 30 15:43:30 2012 +0200 @@ -358,10 +358,6 @@ text {* Simplify, when the exponent is a numeral *} -lemma power_0_left_numeral [simp]: - "0 ^ numeral w = (0::'a::{power,semiring_0})" -by (simp add: power_0_left) - lemmas zero_le_power_eq_numeral [simp] = zero_le_power_eq [of _ "numeral w"] for w