Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove redundant simp rule
authorhuffman
Fri, 30 Mar 2012 15:43:30 +0200
changeset 47225 650318981557
parent 47224 773fe2754b8c
child 47226 ea712316fc87
remove redundant simp rule
src/HOL/Parity.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle