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