# 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