src/HOL/Hyperreal/Lim.thy
changeset 14269 502a7c95de73
parent 13810 c3fbfd472365
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Thu Nov 27 10:47:55 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Fri Nov 28 12:09:37 2003 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4                    differentiation of real=>real functions
     1.5  *)
     1.6  
     1.7 -Lim = SEQ + RealAbs + 
     1.8 +Lim = SEQ + RealArith + 
     1.9  
    1.10  (*-----------------------------------------------------------------------
    1.11      Limits, continuity and differentiation: standard and NS definitions