remove redundant simp rule
authorhuffman
Fri Mar 30 15:43:30 2012 +0200 (2012-03-30)
changeset 47225650318981557
parent 47224 773fe2754b8c
child 47226 ea712316fc87
remove redundant simp rule
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Fri Mar 30 15:24:24 2012 +0200
     1.2 +++ b/src/HOL/Parity.thy	Fri Mar 30 15:43:30 2012 +0200
     1.3 @@ -358,10 +358,6 @@
     1.4  
     1.5  text {* Simplify, when the exponent is a numeral *}
     1.6  
     1.7 -lemma power_0_left_numeral [simp]:
     1.8 -  "0 ^ numeral w = (0::'a::{power,semiring_0})"
     1.9 -by (simp add: power_0_left)
    1.10 -
    1.11  lemmas zero_le_power_eq_numeral [simp] =
    1.12      zero_le_power_eq [of _ "numeral w"] for w
    1.13