# HG changeset patch
# User huffman
# Date 1333115010 -7200
# Node ID 65031898155705705409ebfbe7b8cbb770701e81
# Parent  773fe2754b8c7fc54cfcafae6f764c2cbb9c0744
remove redundant simp rule

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