remove redundant lemmas
authorhuffman
Mon May 14 09:11:30 2007 +0200 (2007-05-14)
changeset 2295907a7c2900877
parent 22958 b3a5569a81e5
child 22960 114cf1906681
remove redundant lemmas
src/HOL/Hyperreal/Series.thy
     1.1 --- a/src/HOL/Hyperreal/Series.thy	Mon May 14 08:15:13 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Series.thy	Mon May 14 09:11:30 2007 +0200
     1.3 @@ -550,7 +550,7 @@
     1.4         in summable_comparison_test)
     1.5  apply (rule_tac x = N in exI, safe)
     1.6  apply (drule le_Suc_ex_iff [THEN iffD1])
     1.7 -apply (auto simp add: power_add realpow_not_zero)
     1.8 +apply (auto simp add: power_add field_power_not_zero)
     1.9  apply (induct_tac "na", auto)
    1.10  apply (rule_tac y = "c * norm (f (N + n))" in order_trans)
    1.11  apply (auto intro: mult_right_mono simp add: summable_def)