# HG changeset patch
# User huffman
# Date 1333025251 -7200
# Node ID 6012241abe938be5d4403072346e9914e4b1b931
# Parent  836bf25fb70f61c84c000bc17961b654556e673c
remove obsolete simp rule for powers

diff -r 836bf25fb70f -r 6012241abe93 src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Thu Mar 29 14:42:55 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy	Thu Mar 29 14:47:31 2012 +0200
@@ -72,14 +72,6 @@
 lemmas numerals = numeral_1_eq_1 [where 'a=nat] numeral_2_eq_2
 
 
-subsection{*Powers with Numeric Exponents*}
-
-text{*Squares of literal numerals will be evaluated.*}
-(* FIXME: replace with more general rules for powers of numerals *)
-lemmas power2_eq_square_numeral [simp] =
-    power2_eq_square [of "numeral w"] for w
-
-
 text{*Simprules for comparisons where common factors can be cancelled.*}
 lemmas zero_compare_simps =
     add_strict_increasing add_strict_increasing2 add_increasing