# HG changeset patch
# User huffman
# Date 1165894294 -3600
# Node ID bf055d30d3adaf3652d6e2d39a5a8bcb38a8ed85
# Parent  8314ebb5364da7c2a7bbce3f8476b0f7db43485a
add type annotation

diff -r 8314ebb5364d -r bf055d30d3ad src/HOL/Hyperreal/MacLaurin.thy
--- 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)