src/HOL/Hyperreal/Series.thy

 imports SEQ
 begin
 
 definition
    sums  :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> bool"
-     (infixr "sums" 80)
+     (infixr "sums" 80) where
    "f sums s = (%n. setsum f {0..<n}) ----> s"
 
-   summable :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool"
+definition
+   summable :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> bool" where
    "summable f = (\<exists>s. f sums s)"
 
-   suminf   :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a"
+definition
+   suminf   :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a" where
    "suminf f = (THE s. f sums s)"
 
 syntax
   "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
 translations