src/HOL/Hyperreal/MacLaurin.thy
changeset 21782 bf055d30d3ad
parent 20792 add17d26151b
child 22983 3314057c3b57
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Dec 12 00:25:09 2006 +0100
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Dec 12 04:31:34 2006 +0100
     1.3 @@ -382,7 +382,7 @@
     1.4  
     1.5  lemma MVT2:
     1.6       "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
     1.7 -      ==> \<exists>z. a < z & z < b & (f b - f a = (b - a) * f'(z))"
     1.8 +      ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
     1.9  apply (drule MVT)
    1.10  apply (blast intro: DERIV_isCont)
    1.11  apply (force dest: order_less_imp_le simp add: differentiable_def)