--- a/src/HOL/Hyperreal/Integration.thy Sat Sep 30 14:32:36 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Sat Sep 30 17:10:55 2006 +0200
@@ -871,6 +871,7 @@
by (blast dest: partition_exists)
lemma monotonic_anti_derivative:
+ fixes f g :: "real => real" shows
"[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
\<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
==> f b - f a \<le> g b - g a"
--- a/src/HOL/Hyperreal/MacLaurin.thy Sat Sep 30 14:32:36 2006 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Sat Sep 30 17:10:55 2006 +0200
@@ -100,6 +100,7 @@
lemma Maclaurin_lemma3:
+ fixes difg :: "nat => real => real" shows
"[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t;
\<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0; n < m; 0 < t;
t < h|]
--- a/src/HOL/Hyperreal/Poly.thy Sat Sep 30 14:32:36 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy Sat Sep 30 17:10:55 2006 +0200
@@ -224,7 +224,7 @@
lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t"
by (simp add: pderiv_def)
-lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c) x :> D * c"
+lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
by (simp add: DERIV_cmult mult_commute [of _ c])
lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
@@ -246,7 +246,7 @@
x ^ n * poly (pderiv_aux (Suc n) p) x "
by (simp add: lemma_DERIV_poly1 del: realpow_Suc)
-lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x) x :> D"
+lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: real) x :> D"
by (rule lemma_DERIV_subst, rule DERIV_add, auto)
lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
--- a/src/HOL/Hyperreal/Series.thy Sat Sep 30 14:32:36 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy Sat Sep 30 17:10:55 2006 +0200
@@ -539,7 +539,7 @@
lemma DERIV_sumr [rule_format (no_asm)]:
"(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
- --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
+ --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
apply (induct "n")
apply (auto intro: DERIV_add)
done