# HG changeset patch
# User huffman
# Date 1234976856 28800
# Node ID 28c5322f0df33a336fbfb8b07392eb3506961fa2
# Parent  ca93255656a5be0ddbb2dd315e823f1b1a6d815f
more subsection headings

diff -r ca93255656a5 -r 28c5322f0df3 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Feb 18 07:24:13 2009 -0800
+++ b/src/HOL/Deriv.thy	Wed Feb 18 09:07:36 2009 -0800
@@ -217,9 +217,7 @@
 by (cases "n", simp, simp add: DERIV_power_Suc f)
 
 
-(* ------------------------------------------------------------------------ *)
-(* Caratheodory formulation of derivative at a point: standard proof        *)
-(* ------------------------------------------------------------------------ *)
+text {* Caratheodory formulation of derivative at a point *}
 
 lemma CARAT_DERIV:
      "(DERIV f x :> l) =
@@ -307,6 +305,9 @@
        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
 by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
 
+lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
+by auto
+
 
 subsection {* Differentiability predicate *}
 
@@ -655,6 +656,9 @@
 apply (blast intro: IVT2)
 done
 
+
+subsection {* Boundedness of continuous functions *}
+
 text{*By bisection, function continuous on closed interval is bounded above*}
 
 lemma isCont_bounded:
@@ -773,6 +777,8 @@
 done
 
 
+subsection {* Local extrema *}
+
 text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
 
 lemma DERIV_left_inc:
@@ -877,6 +883,9 @@
   shows "[| DERIV f x :> l; 0 < d; \<forall>y. \<bar>x-y\<bar> < d --> f(x) = f(y) |] ==> l = 0"
 by (auto dest!: DERIV_local_max)
 
+
+subsection {* Rolle's Theorem *}
+
 text{*Lemma about introducing open ball in open interval*}
 lemma lemma_interval_lt:
      "[| a < x;  x < b |]
@@ -1163,6 +1172,8 @@
 qed
 
 
+subsection {* Continuous injective functions *}
+
 text{*Dull lemma: an continuous injection on an interval must have a
 strict maximum at an end point, not in the middle.*}
 
@@ -1356,6 +1367,9 @@
     using neq by (rule LIM_inverse)
 qed
 
+
+subsection {* Generalized Mean Value Theorem *}
+
 theorem GMVT:
   fixes a b :: real
   assumes alb: "a < b"
@@ -1442,9 +1456,6 @@
   with g'cdef f'cdef cint show ?thesis by auto
 qed
 
-lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
-by auto
-
 
 subsection {* Derivatives of univariate polynomials *}