src/HOL/NSA/HLim.thy
changeset 28562 4e74209f113e
parent 27468 0783dd1dc13d
child 31338 d41a8ba25b67
     1.1 --- a/src/HOL/NSA/HLim.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/NSA/HLim.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -16,18 +16,18 @@
     1.4  definition
     1.5    NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
     1.6              ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
     1.7 -  [code func del]: "f -- a --NS> L =
     1.8 +  [code del]: "f -- a --NS> L =
     1.9      (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
    1.10  
    1.11  definition
    1.12    isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
    1.13      --{*NS definition dispenses with limit notions*}
    1.14 -  [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
    1.15 +  [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
    1.16           ( *f* f) y @= star_of (f a))"
    1.17  
    1.18  definition
    1.19    isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
    1.20 -  [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
    1.21 +  [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
    1.22  
    1.23  
    1.24  subsection {* Limits of Functions *}