src/HOL/Hyperreal/Lim.thy
changeset 14387 e96d5c42c4b0
parent 14269 502a7c95de73
child 14477 cc61fd03e589
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4                    differentiation of real=>real functions
     1.5  *)
     1.6  
     1.7 -Lim = SEQ + RealArith + 
     1.8 +Lim = SEQ + RealDef + 
     1.9  
    1.10  (*-----------------------------------------------------------------------
    1.11      Limits, continuity and differentiation: standard and NS definitions