src/HOL/Series.thy
changeset 44289 d81d09cdab9c
parent 44282 f0de18b62d63
child 44568 e6f291cb5810
     1.1 --- a/src/HOL/Series.thy	Thu Aug 18 18:10:23 2011 -0700
     1.2 +++ b/src/HOL/Series.thy	Thu Aug 18 19:53:03 2011 -0700
     1.3 @@ -26,10 +26,7 @@
     1.4     suminf   :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a" where
     1.5     "suminf f = (THE s. f sums s)"
     1.6  
     1.7 -syntax
     1.8 -  "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
     1.9 -translations
    1.10 -  "\<Sum>i. b" == "CONST suminf (%i. b)"
    1.11 +notation suminf (binder "\<Sum>" 10)
    1.12  
    1.13  
    1.14  lemma [trans]: "f=g ==> g sums z ==> f sums z"
    1.15 @@ -560,7 +557,7 @@
    1.16    moreover have "summable ?g" by (rule summable_zero)
    1.17    moreover from sm have "summable f" .
    1.18    ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
    1.19 -  then show "0 \<le> suminf f" by (simp add: suminf_zero)
    1.20 +  then show "0 \<le> suminf f" by simp
    1.21  qed
    1.22  
    1.23