--- a/src/HOL/Hyperreal/Lim.thy Fri Feb 07 15:36:54 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.thy Fri Feb 07 16:40:23 2003 +0100
@@ -23,7 +23,7 @@
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
"f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a &
x @= hypreal_of_real a -->
- (*f* f) x @= hypreal_of_real L))"
+ ( *f* f) x @= hypreal_of_real L))"
isCont :: [real=>real,real] => bool
"isCont f a == (f -- a --> (f a))"
@@ -31,7 +31,7 @@
(* NS definition dispenses with limit notions *)
isNSCont :: [real=>real,real] => bool
"isNSCont f a == (ALL y. y @= hypreal_of_real a -->
- (*f* f) y @= hypreal_of_real (f a))"
+ ( *f* f) y @= hypreal_of_real (f a))"
(* differentiation: D is derivative of function f at x *)
deriv:: [real=>real,real,real] => bool
@@ -41,7 +41,7 @@
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) +
+ (( *f* f)(hypreal_of_real x + h) +
- hypreal_of_real (f x))/h @= hypreal_of_real D)"
differentiable :: [real=>real,real] => bool (infixl 60)
@@ -52,7 +52,7 @@
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))"
+ inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
isUCont :: (real=>real) => bool
"isUCont f == (ALL r. 0 < r -->
@@ -60,7 +60,7 @@
--> abs(f x + -f y) < r)))"
isNSUCont :: (real=>real) => bool
- "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
+ "isNSUCont f == (ALL x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
(*Used in the proof of the Bolzano theorem*)