--- a/src/HOL/Hyperreal/Deriv.thy Wed May 16 23:03:45 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy Wed May 16 23:07:08 2007 +0200
@@ -12,7 +12,7 @@
imports Lim
begin
-text{*Standard and Nonstandard Definitions*}
+text{*Standard Definitions*}
definition
deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
@@ -38,8 +38,6 @@
subsection {* Derivatives *}
-subsubsection {* Purely standard proofs *}
-
lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
by (simp add: deriv_def)
@@ -326,7 +324,8 @@
==> 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)
-subsubsection {* Differentiability predicate *}
+
+subsection {* Differentiability predicate *}
lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
by (simp add: differentiable_def)
@@ -385,6 +384,7 @@
thus ?thesis by (fold differentiable_def)
qed
+
subsection {* Nested Intervals and Bisection *}
text{*Lemmas about nested intervals and proof by bisection (cf.Harrison).