
diff -r 773fe2754b8c -r 650318981557 src/HOL/Parity.thy
--- 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
 




