src/HOL/Deriv.thy

--- a/src/HOL/Deriv.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Deriv.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -416,10 +416,10 @@
   proof
     fix h show "F h = 0"
     proof (rule ccontr)
-      assume "F h \<noteq> 0"
-      moreover from this have h: "h \<noteq> 0"
+      assume **: "F h \<noteq> 0"
+      then have h: "h \<noteq> 0"
         by (clarsimp simp add: F.zero)
-      ultimately have "0 < ?r h"
+      with ** have "0 < ?r h"
         by (simp add: divide_pos_pos)
       from LIM_D [OF * this] obtain s where s: "0 < s"
         and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
@@ -528,11 +528,11 @@
 lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
 proof safe
   assume "f differentiable x in s"
-  then obtain f' where "FDERIV f x : s :> f'"
+  then obtain f' where *: "FDERIV f x : s :> f'"
     unfolding isDiff_def by auto
-  moreover then obtain c where "f' = (\<lambda>x. x * c)"
+  then obtain c where "f' = (\<lambda>x. x * c)"
     by (metis real_bounded_linear FDERIV_bounded_linear)
-  ultimately show "\<exists>D. DERIV f x : s :> D"
+  with * show "\<exists>D. DERIV f x : s :> D"
     unfolding deriv_fderiv by auto
 qed (auto simp: isDiff_def deriv_fderiv)
 
@@ -730,8 +730,8 @@
     DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
   unfolding DERIV_iff2
 proof (rule filterlim_cong)
-  assume "eventually (\<lambda>x. f x = g x) (nhds x)"
-  moreover then have "f x = g x" by (auto simp: eventually_nhds)
+  assume *: "eventually (\<lambda>x. f x = g x) (nhds x)"
+  moreover from * have "f x = g x" by (auto simp: eventually_nhds)
   moreover assume "x = y" "u = v"
   ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
     by (auto simp: eventually_at_filter elim: eventually_elim1)
@@ -1348,7 +1348,7 @@
 
   {
     from cdef have "?h b - ?h a = (b - a) * l" by auto
-    also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
+    also from leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
     finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
   }
   moreover
@@ -1458,9 +1458,10 @@
       using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less)
     ultimately have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
       using f g `x < a` by (intro GMVT') auto
-    then guess c ..
+    then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c"
+      by blast
     moreover
-    with g'(1)[of c] g'(2) have "(f x - f 0)  / (g x - g 0) = f' c / g' c"
+    from * g'(1)[of c] g'(2) have "(f x - f 0)  / (g x - g 0) = f' c / g' c"
       by (simp add: field_simps)
     ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
       using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])