section labels
authorhuffman
Wed May 16 23:07:08 2007 +0200 (2007-05-16)
changeset 2298467d434ad9ef8
parent 22983 3314057c3b57
child 22985 501e6dfe4e5a
section labels
src/HOL/Hyperreal/Deriv.thy
     1.1 --- a/src/HOL/Hyperreal/Deriv.thy	Wed May 16 23:03:45 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Wed May 16 23:07:08 2007 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  imports Lim
     1.5  begin
     1.6  
     1.7 -text{*Standard and Nonstandard Definitions*}
     1.8 +text{*Standard Definitions*}
     1.9  
    1.10  definition
    1.11    deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
    1.12 @@ -38,8 +38,6 @@
    1.13  
    1.14  subsection {* Derivatives *}
    1.15  
    1.16 -subsubsection {* Purely standard proofs *}
    1.17 -
    1.18  lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
    1.19  by (simp add: deriv_def)
    1.20  
    1.21 @@ -326,7 +324,8 @@
    1.22         ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
    1.23  by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
    1.24  
    1.25 -subsubsection {* Differentiability predicate *}
    1.26 +
    1.27 +subsection {* Differentiability predicate *}
    1.28  
    1.29  lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
    1.30  by (simp add: differentiable_def)
    1.31 @@ -385,6 +384,7 @@
    1.32    thus ?thesis by (fold differentiable_def)
    1.33  qed
    1.34  
    1.35 +
    1.36  subsection {* Nested Intervals and Bisection *}
    1.37  
    1.38  text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).