# HG changeset patch
# User huffman
# Date 1179349628 -7200
# Node ID 67d434ad9ef8346d5f4cfc048890f43225a4cec8
# Parent  3314057c3b575aa1e1adb03863da32ecc1c4e898
section labels

diff -r 3314057c3b57 -r 67d434ad9ef8 src/HOL/Hyperreal/Deriv.thy
--- 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).