1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -5786,7 +5786,7 @@
     1.4      { assume as:"dist a b > dist (f n x) (f n y)"
     1.5        then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
     1.6          and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
     1.7 -        using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_number_of1)
     1.8 +        using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_numeral1)
     1.9        hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
    1.10          apply(erule_tac x="Na+Nb+n" in allE)
    1.11          apply(erule_tac x="Na+Nb+n" in allE) apply simp