# HG changeset patch
# User huffman
# Date 1159629055 -7200
# Node ID add17d26151bebac0f69400ea7f591ffc6645e3f
# Parent  497e1c9d4a9f23cbc25635c2b5d86b0fbb8b64b4
add type annotations for DERIV

diff -r 497e1c9d4a9f -r add17d26151b src/HOL/Hyperreal/Integration.thy
--- 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"
diff -r 497e1c9d4a9f -r add17d26151b src/HOL/Hyperreal/MacLaurin.thy
--- 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|]
diff -r 497e1c9d4a9f -r add17d26151b src/HOL/Hyperreal/Poly.thy
--- 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"
diff -r 497e1c9d4a9f -r add17d26151b src/HOL/Hyperreal/Series.thy
--- 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