src/HOL/Transcendental.thy
changeset 44282 f0de18b62d63
parent 43335 9f8766a8ebe0
child 44289 d81d09cdab9c
     1.1 --- a/src/HOL/Transcendental.thy	Thu Aug 18 17:42:35 2011 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Thu Aug 18 13:36:58 2011 -0700
     1.3 @@ -971,7 +971,7 @@
     1.4  
     1.5  lemma exp_of_real: "exp (of_real x) = of_real (exp x)"
     1.6  unfolding exp_def
     1.7 -apply (subst of_real.suminf)
     1.8 +apply (subst suminf_of_real)
     1.9  apply (rule summable_exp_generic)
    1.10  apply (simp add: scaleR_conv_of_real)
    1.11  done