diff -r 2a03ae772c60 -r 8020249565fb src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Sep 13 14:44:03 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Sep 13 16:50:12 2015 +0200
@@ -1191,8 +1191,9 @@
   have lem1: "\<forall>e>0. \<exists>d>0. \<forall>z.
     norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
   proof (rule, rule)
-    case goal1
-    have *: "e / C > 0" using \<open>e > 0\<close> C(1) by auto
+    fix e :: real
+    assume "e > 0"
+    with C(1) have *: "e / C > 0" by auto
     obtain d0 where d0:
         "0 < d0"
         "\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)"
@@ -1213,7 +1214,7 @@
       using assms(6) by blast
     obtain d where d: "0 < d" "d < d1" "d < d2"
       using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
-    then show ?case
+    then show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
       apply (rule_tac x=d in exI)
       apply rule
       defer
@@ -1257,14 +1258,13 @@
   def B \<equiv> "C * 2"
   have "B > 0"
     unfolding B_def using C by auto
-  have lem2: "\<forall>z. norm(z - y) < d \<longrightarrow> norm (g z - g y) \<le> B * norm (z - y)"
-  proof (rule, rule)
-    case goal1
+  have lem2: "norm (g z - g y) \<le> B * norm (z - y)" if z: "norm(z - y) < d" for z
+  proof -
     have "norm (g z - g y) \<le> norm(g' (z - y)) + norm ((g z - g y) - g'(z - y))"
       by (rule norm_triangle_sub)
     also have "\<dots> \<le> norm (g' (z - y)) + 1 / 2 * norm (g z - g y)"
       apply (rule add_left_mono)
-      using d and goal1
+      using d and z
       apply auto
       done
     also have "\<dots> \<le> norm (z - y) * C + 1 / 2 * norm (g z - g y)"
@@ -1272,7 +1272,7 @@
       using C
       apply auto
       done
-    finally show ?case
+    finally show "norm (g z - g y) \<le> B * norm (z - y)"
       unfolding B_def
       by (auto simp add: field_simps)
   qed
@@ -1283,15 +1283,16 @@
     apply rule
     apply rule
   proof -
-    case goal1
-    hence *: "e / B >0" by (metis \<open>0 < B\<close> divide_pos_pos)
+    fix e :: real
+    assume "e > 0"
+    then have *: "e / B > 0" by (metis \<open>B > 0\<close> divide_pos_pos)
     obtain d' where d':
         "0 < d'"
         "\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
       using lem1 * by blast
     obtain k where k: "0 < k" "k < d" "k < d'"
       using real_lbound_gt_zero[OF d(1) d'(1)] by blast
-    show ?case
+    show "\<exists>d>0. \<forall>ya. norm (ya - y) < d \<longrightarrow> norm (g ya - g y - g' (ya - y)) \<le> e * norm (ya - y)"
       apply (rule_tac x=k in exI)
       apply auto
     proof -
@@ -1301,7 +1302,7 @@
         using d' k by auto
       also have "\<dots> \<le> e * norm (z - y)"
         unfolding times_divide_eq_left pos_divide_le_eq[OF \<open>B>0\<close>]
-        using lem2[THEN spec[where x=z]]
+        using lem2[of z]
         using k as using \<open>e > 0\<close>
         by (auto simp add: field_simps)
       finally show "norm (g z - g y - g' (z - y)) \<le> e * norm (z - y)"
@@ -1650,7 +1651,8 @@
       apply rule
       apply rule
     proof -
-      case goal1
+      fix y
+      assume "0 < dist y (f x) \<and> dist y (f x) < d"
       then have "g y \<in> g ` f ` (ball x e \<inter> s)"
         using d(2)[unfolded subset_eq,THEN bspec[where x=y]]
         by (auto simp add: dist_commute)
@@ -1667,13 +1669,12 @@
     using interior_open[OF assms(1)] and \<open>x \<in> s\<close>
     apply auto
     done
-  moreover have "\<And>y. y \<in> interior (f ` s) \<Longrightarrow> f (g y) = y"
+  moreover have "f (g y) = y" if "y \<in> interior (f ` s)" for y
   proof -
-    case goal1
-    then have "y \<in> f ` s"
+    from that have "y \<in> f ` s"
       using interior_subset by auto
     then obtain z where "z \<in> s" "y = f z" unfolding image_iff ..
-    then show ?case
+    then show ?thesis
       using assms(4) by auto
   qed
   ultimately show ?thesis using assms
@@ -1882,11 +1883,13 @@
   shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s.
     norm ((f m x - f n x) - (f m y - f n y)) \<le> e * norm (x - y)"
 proof (rule, rule)
-  case goal1 have *: "2 * (1/2* e) = e" "1/2 * e >0"
-    using \<open>e > 0\<close> by auto
+  fix e :: real
+  assume "e > 0"
+  then have *: "2 * (1/2* e) = e" "1/2 * e >0"
+    by auto
   obtain N where "\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> 1 / 2 * e * norm h"
     using assms(3) *(2) by blast
-  then show ?case
+  then show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm (f m x - f n x - (f m y - f n y)) \<le> e * norm (x - y)"
     apply (rule_tac x=N in exI)
     apply (rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *])
     using assms \<open>e > 0\<close>
@@ -2060,9 +2063,10 @@
     qed
     show "\<forall>e>0. eventually (\<lambda>y. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)) (at x within s)"
     proof (rule, rule)
-      case goal1
-      have *: "e / 3 > 0"
-        using goal1 by auto
+      fix e :: real
+      assume "e > 0"
+      then have *: "e / 3 > 0"
+        by auto
       obtain N1 where N1: "\<forall>n\<ge>N1. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e / 3 * norm h"
         using assms(3) * by blast
       obtain N2 where
@@ -2073,7 +2077,7 @@
         using assms(2)[unfolded has_derivative_within_alt2] and \<open>x \<in> s\<close> and * by fast
       moreover have "eventually (\<lambda>y. y \<in> s) (at x within s)"
         unfolding eventually_at by (fast intro: zero_less_one)
-      ultimately show ?case
+      ultimately show "\<forall>\<^sub>F y in at x within s. norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)"
       proof (rule eventually_elim2)
         fix y
         assume "y \<in> s"
@@ -2150,15 +2154,20 @@
       using reals_Archimedean[OF \<open>e>0\<close>] ..
     show "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm (f' n x h - g' x h) \<le> e * norm h"
       apply (rule_tac x=N in exI)
-    proof rule+
-      case goal1
+      apply rule
+      apply rule
+      apply rule
+      apply rule
+    proof -
+      fix n x h
+      assume n: "N \<le> n" and x: "x \<in> s"
       have *: "inverse (real (Suc n)) \<le> e"
         apply (rule order_trans[OF _ N[THEN less_imp_le]])
-        using goal1(1)
+        using n
         apply (auto simp add: field_simps)
         done
-      show ?case
-        using f[rule_format,THEN conjunct2,OF goal1(2), of n, THEN spec[where x=h]]
+      show "norm (f' n x h - g' x h) \<le> e * norm h"
+        using f[rule_format,THEN conjunct2, OF x, of n, THEN spec[where x=h]]
         apply (rule order_trans)
         using N *
         apply (cases "h = 0")