src/HOL/Hyperreal/Series.thy
changeset 20552 2c31dd358c21
parent 20432 07ec57376051
child 20688 690d866a165d
     1.1 --- a/src/HOL/Hyperreal/Series.thy	Sat Sep 16 02:35:58 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/Series.thy	Sat Sep 16 02:40:00 2006 +0200
     1.3 @@ -354,7 +354,7 @@
     1.4  apply (drule spec, drule (1) mp)
     1.5  apply (erule exE, rule_tac x="N" in exI, clarify)
     1.6  apply (rule_tac x="m" and y="n" in linorder_le_cases)
     1.7 -apply (subst abs_minus_commute)
     1.8 +apply (subst norm_minus_commute)
     1.9  apply (simp add: setsum_diff [symmetric])
    1.10  apply (simp add: setsum_diff [symmetric])
    1.11  done