1.1 --- a/src/HOL/NSA/HSeries.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/NSA/HSeries.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  definition
     1.6    sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
     1.7 -  [code func del]: "sumhr = 
     1.8 +  [code del]: "sumhr = 
     1.9        (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
    1.10  
    1.11  definition
    1.12 @@ -22,7 +22,7 @@
    1.13  
    1.14  definition
    1.15    NSsummable :: "(nat=>real) => bool" where
    1.16 -  [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
    1.17 +  [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
    1.18  
    1.19  definition
    1.20    NSsuminf   :: "(nat=>real) => real" where