src/HOL/Hyperreal/Lim.thy

 
 constdefs
   LIM :: [real=>real,real,real] => bool
 				("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
   "f -- a --> L ==
-     ALL r. Numeral0 < r --> 
-	     (EX s. Numeral0 < s & (ALL x. (x ~= a & (abs(x + -a) < s)
+     ALL r. 0 < r --> 
+	     (EX s. 0 < s & (ALL x. (x ~= a & (abs(x + -a) < s)
 			  --> abs(f x + -L) < r)))"
 
   NSLIM :: [real=>real,real,real] => bool
 			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
   "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & 

 			   (*f* f) y @= hypreal_of_real (f a))"
 
   (* differentiation: D is derivative of function f at x *)
   deriv:: [real=>real,real,real] => bool
 			    ("(DERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
-  "DERIV f x :> D == ((%h. (f(x + h) + -f(x))/h) -- Numeral0 --> D)"
+  "DERIV f x :> D == ((%h. (f(x + h) + -f(x))/h) -- 0 --> D)"
 
   nsderiv :: [real=>real,real,real] => bool
 			    ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
   "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. 
 			((*f* f)(hypreal_of_real x + h) + 

   increment :: [real=>real,real,hypreal] => hypreal
   "increment f x h == (@inc. f NSdifferentiable x & 
 		       inc = (*f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
 
   isUCont :: (real=>real) => bool
-  "isUCont f ==  (ALL r. Numeral0 < r --> 
-		      (EX s. Numeral0 < s & (ALL x y. abs(x + -y) < s
+  "isUCont f ==  (ALL r. 0 < r --> 
+		      (EX s. 0 < s & (ALL x y. abs(x + -y) < s
 			    --> abs(f x + -f y) < r)))"
 
   isNSUCont :: (real=>real) => bool
   "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"