# HG changeset patch
# User wenzelm
# Date 1442168416 -7200
# Node ID 5976fe402824c603ae7b16bf14594428f64c846d
# Parent  8020249565fb2be7e848076bfc3222c14020fbb0
renamed method "goals" to "goal_cases" to emphasize its meaning;

diff -r 8020249565fb -r 5976fe402824 NEWS
--- a/NEWS	Sun Sep 13 16:50:12 2015 +0200
+++ b/NEWS	Sun Sep 13 20:20:16 2015 +0200
@@ -116,13 +116,13 @@
 sequences. Further explanations and examples are given in the isar-ref
 manual.
 
-* Proof method "goals" turns the current subgoals into cases within the
-context; the conclusion is bound to variable ?case in each case.
-For example:
+* Proof method "goal_cases" turns the current subgoals into cases within
+the context; the conclusion is bound to variable ?case in each case. For
+example:
 
 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
-proof goals
+proof goal_cases
   case (1 x)
   then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
 next
@@ -132,7 +132,7 @@
 
 lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
   and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
-proof goals
+proof goal_cases
   case prems: 1
   then show ?case using prems sorry
 next
diff -r 8020249565fb -r 5976fe402824 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -832,7 +832,7 @@
   \begin{matharray}{rcl}
     @{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
     @{method_def "-"} & : & @{text method} \\
-    @{method_def "goals"} & : & @{text method} \\
+    @{method_def "goal_cases"} & : & @{text method} \\
     @{method_def "fact"} & : & @{text method} \\
     @{method_def "assumption"} & : & @{text method} \\
     @{method_def "this"} & : & @{text method} \\
@@ -847,7 +847,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{method goals} (@{syntax name}*)
+    @@{method goal_cases} (@{syntax name}*)
     ;
     @@{method fact} @{syntax thmrefs}?
     ;
@@ -886,7 +886,7 @@
   method; thus a plain \emph{do-nothing} proof step would be ``@{command
   "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
 
-  \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
+  \item @{method "goal_cases"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
   into cases within the context (see also \secref{sec:cases-induct}). The
   specified case names are used if present; otherwise cases are numbered
   starting from 1.
diff -r 8020249565fb -r 5976fe402824 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -578,7 +578,7 @@
 begin
 
 sublocale dlo: unbounded_dense_linorder
-proof (unfold_locales, goals)
+proof (unfold_locales, goal_cases)
   case (1 x y)
   then show ?case
     using between_less [of x y] by auto
diff -r 8020249565fb -r 5976fe402824 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -891,7 +891,7 @@
 subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution  etc ...\<close>
 
 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
-proof (induct p arbitrary: n rule: poly.induct, auto, goals)
+proof (induct p arbitrary: n rule: poly.induct, auto, goal_cases)
   case prems: (1 c n p n')
   then have "n = Suc (n - 1)"
     by simp
diff -r 8020249565fb -r 5976fe402824 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -479,7 +479,7 @@
   and "eq_set (set ys) (List.coset xs) \<longleftrightarrow> rhs"
   and "eq_set (set xs) (set ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
   and "eq_set (List.coset xs) (List.coset ys) \<longleftrightarrow> (\<forall>x \<in> set xs. x \<in> set ys) \<and> (\<forall>y \<in> set ys. y \<in> set xs)"
-proof goals
+proof goal_cases
   {
     case 1
     show ?case (is "?lhs \<longleftrightarrow> ?rhs")
diff -r 8020249565fb -r 5976fe402824 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -333,7 +333,7 @@
 | "ereal r + -\<infinity> = - \<infinity>"
 | "-\<infinity> + ereal p = -(\<infinity>::ereal)"
 | "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
-proof goals
+proof goal_cases
   case prems: (1 P x)
   then obtain a b where "x = (a, b)"
     by (cases x) auto
@@ -437,7 +437,7 @@
 | "ereal x    < \<infinity>           \<longleftrightarrow> True"
 | "        -\<infinity> < ereal r     \<longleftrightarrow> True"
 | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
-proof goals
+proof goal_cases
   case prems: (1 P x)
   then obtain a b where "x = (a,b)" by (cases x) auto
   with prems show P by (cases rule: ereal2_cases[of a b]) auto
@@ -860,7 +860,7 @@
 | "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
 | "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
 | "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
-proof goals
+proof goal_cases
   case prems: (1 P x)
   then obtain a b where "x = (a, b)"
     by (cases x) auto
diff -r 8020249565fb -r 5976fe402824 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Library/Product_Order.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -233,7 +233,7 @@
 (* Contribution: Alessandro Coglio *)
 
 instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof (standard, goals)
+proof (standard, goal_cases)
   case 1
   then show ?case
     by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
diff -r 8020249565fb -r 5976fe402824 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -157,7 +157,7 @@
     note b = this(1) and body = this(2) and inv = this(3)
     hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
     ultimately show ?thesis unfolding Suc using b
-    proof (intro Least_equality[symmetric], goals)
+    proof (intro Least_equality[symmetric], goal_cases)
       case 1
       hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
         by (auto simp: BodyCommute inv b)
diff -r 8020249565fb -r 5976fe402824 src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -175,7 +175,7 @@
   qed
   have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
     unfolding subset_eq
-  proof (rule, goals)
+  proof (rule, goal_cases)
     case (1 x)
     then obtain y :: "real^2" where y:
         "y \<in> cbox (- 1) 1"
@@ -834,7 +834,7 @@
       z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
       z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
       z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
-    proof (simp only: segment_vertical segment_horizontal vector_2, goals)
+    proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
       case as: 1
       have "pathfinish f \<in> cbox a b"
         using assms(3) pathfinish_in_path_image[of f] by auto 
diff -r 8020249565fb -r 5976fe402824 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -2392,7 +2392,7 @@
   have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
     (f has_integral y) (cbox a b) \<Longrightarrow> ((h o f) has_integral h y) (cbox a b)"
     unfolding has_integral
-  proof (clarify, goals)
+  proof (clarify, goal_cases)
     case (1 f y a b e)
     from pos_bounded
     obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
@@ -2441,7 +2441,7 @@
       using has_integral_altD[OF assms(1) as *] by blast
     show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
       (\<exists>z. ((\<lambda>x. if x \<in> s then (h \<circ> f) x else 0) has_integral z) (cbox a b) \<and> norm (z - h y) < e)"
-    proof (rule_tac x=M in exI, clarsimp simp add: M, goals)
+    proof (rule_tac x=M in exI, clarsimp simp add: M, goal_cases)
       case (1 a b)
       obtain z where z:
         "((\<lambda>x. if x \<in> s then f x else 0) has_integral z) (cbox a b)"
@@ -2553,7 +2553,7 @@
   }
   assume as: "\<not> (\<exists>a b. s = cbox a b)"
   then show ?thesis
-  proof (subst has_integral_alt, clarsimp, goals)
+  proof (subst has_integral_alt, clarsimp, goal_cases)
     case (1 e)
     then have *: "e / 2 > 0"
       by auto
@@ -2809,7 +2809,7 @@
   assume ?l
   then guess y unfolding integrable_on_def has_integral .. note y=this
   show "\<forall>e>0. \<exists>d. ?P e d"
-  proof (clarify, goals)
+  proof (clarify, goal_cases)
     case (1 e)
     then have "e/2 > 0" by auto
     then guess d
@@ -2844,7 +2844,7 @@
   have dp: "\<And>i n. i\<le>n \<Longrightarrow> d i fine p n"
     using p(2) unfolding fine_inters by auto
   have "Cauchy (\<lambda>n. setsum (\<lambda>(x,k). content k *\<^sub>R (f x)) (p n))"
-  proof (rule CauchyI, goals)
+  proof (rule CauchyI, goal_cases)
     case (1 e)
     then guess N unfolding real_arch_inv[of e] .. note N=this
     show ?case
@@ -3104,7 +3104,7 @@
       and fj: "(f has_integral j) (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
       and k: "k \<in> Basis"
   shows "(f has_integral (i + j)) (cbox a b)"
-proof (unfold has_integral, rule, rule, goals)
+proof (unfold has_integral, rule, rule, goal_cases)
   case (1 e)
   then have e: "e/2 > 0"
     by auto
@@ -4748,7 +4748,7 @@
   assumes k: "k \<in> Basis"
   shows "negligible {x. x\<bullet>k = c}"
   unfolding negligible_def has_integral
-proof (clarify, goals)
+proof (clarify, goal_cases)
   case (1 a b e)
   from this and k obtain d where d: "0 < d" "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
     by (rule content_doublesplit)
@@ -4823,7 +4823,7 @@
         apply (auto simp add:interval_doublesplit[OF k])
         done
       also have "\<dots> < e"
-      proof (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]], goals)
+      proof (subst setsum_over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
         case (1 u v)
         have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
           unfolding interval_doublesplit[OF k]
@@ -5112,7 +5112,7 @@
   assume assm: "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
   show "(f has_integral 0) (cbox a b)"
     unfolding has_integral
-  proof (safe, goals)
+  proof (safe, goal_cases)
     case (1 e)
     then have "\<And>n. e / 2 / ((real n+1) * (2 ^ n)) > 0"
       apply -
@@ -5240,7 +5240,7 @@
           done
       qed (insert as, auto)
       also have "\<dots> \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {..N+1}"
-      proof (rule setsum_mono, goals)
+      proof (rule setsum_mono, goal_cases)
         case (1 i)
         then show ?case
           apply (subst mult.commute, subst pos_le_divide_eq[symmetric])
@@ -5347,7 +5347,7 @@
     and "t \<subseteq> s"
   shows "negligible t"
   unfolding negligible_def
-proof (safe, goals)
+proof (safe, goal_cases)
   case (1 a b)
   show ?case
     using assms(1)[unfolded negligible_def,rule_format,of a b]
@@ -5376,7 +5376,7 @@
     and "negligible t"
   shows "negligible (s \<union> t)"
   unfolding negligible_def
-proof (safe, goals)
+proof (safe, goal_cases)
   case (1 a b)
   note assm = assms[unfolded negligible_def,rule_format,of a b]
   then show ?case
@@ -5584,7 +5584,7 @@
   show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
     apply (rule_tac x="?g" in exI)
     apply safe
-  proof goals
+  proof goal_cases
     case (1 x)
     then show ?case
       apply -
@@ -6074,7 +6074,7 @@
     "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
   and taylor_integrable:
     "i integrable_on {a .. b}"
-proof goals
+proof goal_cases
   case 1
   interpret bounded_bilinear "scaleR::real\<Rightarrow>'a\<Rightarrow>'a"
     by (rule bounded_bilinear_scaleR)
@@ -6431,7 +6431,7 @@
   let ?I = "\<lambda>a b. integral {a .. b} f"
   show "\<exists>d>0. \<forall>y\<in>{a .. b}. norm (y - x) < d \<longrightarrow>
     norm (?I a y - ?I a x - (y - x) *\<^sub>R f x) \<le> e * norm (y - x)"
-  proof (rule, rule, rule d, safe, goals)
+  proof (rule, rule, rule d, safe, goal_cases)
     case (1 y)
     show ?case
     proof (cases "y < x")
@@ -6565,7 +6565,7 @@
   show ?thesis
     apply (rule that[of g])
     apply safe
-  proof goals
+  proof goal_cases
     case (1 u v)
     have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
       apply rule
@@ -6598,7 +6598,7 @@
     defer
     apply (rule *)
     apply assumption
-  proof goals
+  proof goal_cases
     case 1
     then show ?thesis
       unfolding 1 assms(8)[unfolded 1 has_integral_empty_eq] by auto
@@ -7185,7 +7185,7 @@
   let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
   show "?P e"
     apply (rule_tac x="?d" in exI)
-  proof (safe, goals)
+  proof (safe, goal_cases)
     case 1
     show ?case
       apply (rule gauge_ball_dependent)
@@ -7207,7 +7207,7 @@
       apply (subst(2) pA)
       apply (subst pA)
       unfolding setsum.union_disjoint[OF pA(2-)]
-    proof (rule norm_triangle_le, rule **, goals)
+    proof (rule norm_triangle_le, rule **, goal_cases)
       case 1
       show ?case
         apply (rule order_trans)
@@ -7295,7 +7295,7 @@
           defer
           apply rule
           unfolding split_paired_all split_conv o_def
-        proof goals
+        proof goal_cases
           fix x k
           assume "(x, k) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> {t. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
           then have xk: "(x, k) \<in> p" "content k = 0"
@@ -7450,7 +7450,7 @@
               apply rule
               unfolding mem_Collect_eq
               unfolding split_paired_all fst_conv snd_conv
-            proof (safe, goals)
+            proof (safe, goal_cases)
               case 1
               guess v using pa[OF 1(1)] .. note v = conjunctD2[OF this]
               have "?a \<in> {?a..v}"
@@ -7482,7 +7482,7 @@
               apply rule
               unfolding mem_Collect_eq
               unfolding split_paired_all fst_conv snd_conv
-            proof (safe, goals)
+            proof (safe, goal_cases)
               case 1
               guess v using pb[OF 1(1)] .. note v = conjunctD2[OF this]
               have "?b \<in> {v.. ?b}"
@@ -7698,7 +7698,7 @@
     from fine_division_exists_real[OF this, of a t] guess p . note p=this
     note p'=tagged_division_ofD[OF this(1)]
     have pt: "\<forall>(x,k)\<in>p. x \<le> t"
-    proof (safe, goals)
+    proof (safe, goal_cases)
       case 1
       from p'(2,3)[OF this] show ?case
         by auto
@@ -7753,7 +7753,7 @@
       have **: "\<And>x F. F \<union> {x} = insert x F"
         by auto
       have "(c, cbox t c) \<notin> p"
-      proof (safe, goals)
+      proof (safe, goal_cases)
         case 1
         from p'(2-3)[OF this] have "c \<in> cbox a t"
           by auto
@@ -7855,7 +7855,7 @@
       apply cases
       apply (rule *)
       apply assumption
-    proof goals
+    proof goal_cases
       case 1
       then have "cbox a b = {x}"
         using as(1)
@@ -8143,7 +8143,7 @@
       apply cases
       apply (rule *)
       apply assumption
-    proof goals
+    proof goal_cases
       case 1
       then have *: "box c d = {}"
         by (metis bot.extremum_uniqueI box_subset_cbox)
@@ -8347,7 +8347,7 @@
     have "ball 0 C \<subseteq> cbox c d"
       apply (rule subsetI)
       unfolding mem_box mem_ball dist_norm
-    proof (rule, goals)
+    proof (rule, goal_cases)
       fix x i :: 'n
       assume x: "norm (0 - x) < C" and i: "i \<in> Basis"
       show "c \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> d \<bullet> i"
@@ -8658,7 +8658,7 @@
   show ?l
     apply (subst has_integral')
     apply safe
-  proof goals
+  proof goal_cases
     case (1 e)
     from \<open>?r\<close>[THEN conjunct2,rule_format,OF this] guess B .. note B=conjunctD2[OF this]
     show ?case
@@ -8686,7 +8686,7 @@
       have "ball 0 B \<subseteq> cbox ?a ?b"
         apply (rule subsetI)
         unfolding mem_ball mem_box dist_norm
-      proof (rule, goals)
+      proof (rule, goal_cases)
         case (1 x i)
         then show ?case using Basis_le_norm[of i x]
           by (auto simp add:field_simps)
@@ -8712,7 +8712,7 @@
       apply rule
       apply (rule B)
       apply safe
-    proof goals
+    proof goal_cases
       case 1
       from B(2)[OF this] guess z .. note z=conjunctD2[OF this]
       from integral_unique[OF this(1)] show ?case
@@ -8739,7 +8739,7 @@
   show ?r
     apply safe
     apply (rule y)
-  proof goals
+  proof goal_cases
     case (1 e)
     then have "e/2 > 0"
       by auto
@@ -8749,7 +8749,7 @@
       apply rule
       apply (rule B)
       apply safe
-    proof goals
+    proof goal_cases
       case (1 a b c d)
       show ?case
         apply (rule norm_triangle_half_l)
@@ -8763,7 +8763,7 @@
   note as = conjunctD2[OF this,rule_format]
   let ?cube = "\<lambda>n. cbox (\<Sum>i\<in>Basis. - real n *\<^sub>R i::'n) (\<Sum>i\<in>Basis. real n *\<^sub>R i)"
   have "Cauchy (\<lambda>n. integral (?cube n) (\<lambda>x. if x \<in> s then f x else 0))"
-  proof (unfold Cauchy_def, safe, goals)
+  proof (unfold Cauchy_def, safe, goal_cases)
     case (1 e)
     from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
     from real_arch_simple[of B] guess N .. note N = this
@@ -8773,7 +8773,7 @@
       have "ball 0 B \<subseteq> ?cube n"
         apply (rule subsetI)
         unfolding mem_ball mem_box dist_norm
-      proof (rule, goals)
+      proof (rule, goal_cases)
         case (1 x i)
         then show ?case
           using Basis_le_norm[of i x] \<open>i\<in>Basis\<close>
@@ -8797,7 +8797,7 @@
     apply (rule_tac x=i in exI)
     apply safe
     apply (rule as(1)[unfolded integrable_on_def])
-  proof goals
+  proof goal_cases
     case (1 e)
     then have *: "e/2 > 0" by auto
     from i[OF this] guess N .. note N =this[rule_format]
@@ -8830,7 +8830,7 @@
           using x
           unfolding mem_box mem_ball dist_norm
           apply -
-        proof (rule, goals)
+        proof (rule, goal_cases)
           case (1 i)
           then show ?case
             using Basis_le_norm[of i x] \<open>i \<in> Basis\<close>
@@ -8870,7 +8870,7 @@
   assumes "\<forall>e>0. \<exists>g  h i j. (g has_integral i) (cbox a b) \<and> (h has_integral j) (cbox a b) \<and>
     norm (i - j) < e \<and> (\<forall>x\<in>cbox a b. (g x) \<le> f x \<and> f x \<le> h x)"
   shows "f integrable_on cbox a b"
-proof (subst integrable_cauchy, safe, goals)
+proof (subst integrable_cauchy, safe, goal_cases)
   case (1 e)
   then have e: "e/3 > 0"
     by auto
@@ -8882,7 +8882,7 @@
     apply (rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI)
     apply (rule conjI gauge_inter d1 d2)+
     unfolding fine_inter
-  proof (safe, goals)
+  proof (safe, goal_cases)
     have **: "\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
       abs (i - j) < e / 3 \<Longrightarrow> abs (g2 - i) < e / 3 \<Longrightarrow>  abs (g1 - i) < e / 3 \<Longrightarrow>
       abs (h2 - j) < e / 3 \<Longrightarrow> abs (h1 - j) < e / 3 \<Longrightarrow> abs (f1 - f2) < e"
@@ -8949,7 +8949,7 @@
   shows "f integrable_on s"
 proof -
   have "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on cbox a b"
-  proof (rule integrable_straddle_interval, safe, goals)
+  proof (rule integrable_straddle_interval, safe, goal_cases)
     case (1 a b e)
     then have *: "e/4 > 0"
       by auto
@@ -8968,7 +8968,7 @@
       apply safe
       unfolding mem_ball mem_box dist_norm
       apply (rule_tac[!] ballI)
-    proof goals
+    proof goal_cases
       case (1 x i)
       then show ?case using Basis_le_norm[of i x]
         unfolding c_def d_def by auto
@@ -9027,7 +9027,7 @@
     unfolding integrable_alt[of f]
     apply safe
     apply (rule interv)
-  proof goals
+  proof goal_cases
     case (1 e)
     then have *: "e/3 > 0"
       by auto
@@ -9132,7 +9132,7 @@
     defer
     apply assumption
     apply safe
-  proof goals
+  proof goal_cases
     case (1 x)
     then show ?case
     proof (cases "x \<in> \<Union>t")
@@ -9174,7 +9174,7 @@
     apply rule
     apply rule
     apply rule
-  proof goals
+  proof goal_cases
     case (1 s s')
     from d(4)[OF this(1)] d(4)[OF this(2)] guess a c b d by (elim exE) note obt=this
     from d(5)[OF 1] show ?case
@@ -9208,7 +9208,7 @@
   apply (rule has_integral_combine_division[OF assms(2)])
   apply safe
   unfolding has_integral_integral[symmetric]
-proof goals
+proof goal_cases
   case (1 k)
   from division_ofD(2,4)[OF assms(2) this]
   show ?case
@@ -9248,7 +9248,7 @@
   shows "f integrable_on i"
   apply (rule integrable_combine_division assms)+
   apply safe
-proof goals
+proof goal_cases
   case 1
   note division_ofD(2,4)[OF assms(1) this]
   then show ?case
@@ -9310,7 +9310,7 @@
   shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) (cbox a b)"
   apply (rule has_integral_combine_tagged_division[OF assms(2)])
   apply safe
-proof goals
+proof goal_cases
   case 1
   note tagged_division_ofD(3-4)[OF assms(2) this]
   then show ?case
@@ -9359,7 +9359,7 @@
   have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
     norm (setsum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
     apply safe
-  proof goals
+  proof goal_cases
     case (1 i)
     then have i: "i \<in> q"
       unfolding r_def by auto
@@ -9398,7 +9398,7 @@
     note * = tagged_partial_division_of_union_self[OF p(1)]
     have "p \<union> \<Union>(qq ` r) tagged_division_of \<Union>(snd ` p) \<union> \<Union>r"
       using r
-    proof (rule tagged_division_union[OF * tagged_division_unions], goals)
+    proof (rule tagged_division_union[OF * tagged_division_unions], goal_cases)
       case 1
       then show ?case
         using qq by auto
@@ -9534,7 +9534,7 @@
     unfolding split_def setsum_subtractf ..
   also have "\<dots> \<le> e + k"
     apply (rule *[OF **, where ir2="setsum (\<lambda>k. integral k f) r"])
-  proof goals
+  proof goal_cases
     case 2
     have *: "(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
       apply (subst setsum.reindex_nontrivial)
@@ -9620,7 +9620,7 @@
   show thesis
     apply (rule that)
     apply (rule d)
-  proof (safe, goals)
+  proof (safe, goal_cases)
     case (1 p)
     note * = henstock_lemma_part2[OF assms(1) * d this]
     show ?case
@@ -9776,7 +9776,7 @@
 
   have "(g has_integral i) (cbox a b)"
     unfolding has_integral
-  proof (safe, goals)
+  proof (safe, goal_cases)
     case e: (1 e)
     then have "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
       norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral (cbox a b) (f k)) < e / 2 ^ (k + 2)))"
@@ -9803,7 +9803,7 @@
 
     have "\<forall>x\<in>cbox a b. \<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)\<bullet>1 - (f k x)\<bullet>1 \<and>
       (g x)\<bullet>1 - (f k x)\<bullet>1 < e / (4 * content(cbox a b))"
-    proof (rule, goals)
+    proof (rule, goal_cases)
       case (1 x)
       have "e / (4 * content (cbox a b)) > 0"
         using \<open>e>0\<close> False content_pos_le[of a b] by auto
@@ -9835,7 +9835,7 @@
       then guess s .. note s=this
       have *: "\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e / 2 \<and>
         norm (c - d) < e / 4 \<longrightarrow> norm (a - d) < e"
-      proof (safe, goals)
+      proof (safe, goal_cases)
         case (1 a b c d)
         then show ?case
           using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
@@ -9846,7 +9846,7 @@
       show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e"
         apply (rule *[rule_format,where
           b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"])
-      proof (safe, goals)
+      proof (safe, goal_cases)
         case 1
         show ?case
           apply (rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content (cbox a b)))"])
@@ -10062,7 +10062,7 @@
     have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
       ((\<lambda>k. integral (cbox a b) (\<lambda>x. if x \<in> s then f k x else 0)) --->
       integral (cbox a b) (\<lambda>x. if x \<in> s then g x else 0)) sequentially"
-    proof (rule monotone_convergence_interval, safe, goals)
+    proof (rule monotone_convergence_interval, safe, goal_cases)
       case 1
       show ?case by (rule int)
     next
@@ -10117,7 +10117,7 @@
       unfolding has_integral_alt'
       apply safe
       apply (rule g(1))
-    proof goals
+    proof goal_cases
       case (1 e)
       then have "e/4>0"
         by auto
@@ -10155,7 +10155,7 @@
           apply (rule integral_le[OF int int])
           defer
           apply (rule order_trans[OF _ i'[rule_format,of "M + N",unfolded real_inner_1_right]])
-        proof (safe, goals)
+        proof (safe, goal_cases)
           case (2 x)
           have "\<And>m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
             apply (rule transitive_stepwise_le)
@@ -10200,7 +10200,7 @@
     integral s (\<lambda>x. g x - f 0 x)) sequentially"
     apply (rule lem)
     apply safe
-  proof goals
+  proof goal_cases
     case (1 k x)
     then show ?case
       using *[of x 0 "Suc k"] by auto
@@ -10538,7 +10538,7 @@
   obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   apply (rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
   apply safe
-proof goals
+proof goal_cases
   case (1 d)
   note d = division_ofD[OF 1(2)]
   have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
@@ -10591,7 +10591,7 @@
     apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
     apply (subst has_integral[of _ ?S])
     apply safe
-  proof goals
+  proof goal_cases
     case (1 e)
     then have "?S - e / 2 < ?S" by simp
     then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
@@ -10725,7 +10725,7 @@
         by (force intro!: helplemma)
 
       have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
-      proof (safe, goals)
+      proof (safe, goal_cases)
         case (2 _ _ x i l)
         have "x \<in> i"
           using fineD[OF p(3) 2(1)] k(2)[OF 2(2), of x] 2(4-)
@@ -10773,7 +10773,7 @@
         apply (rule *[rule_format,OF **])
         apply safe
         apply(rule d(2))
-      proof goals
+      proof goal_cases
         case 1
         show ?case
           by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
@@ -10783,7 +10783,7 @@
           (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
           by auto
         have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
-        proof (rule setsum_mono, goals)
+        proof (rule setsum_mono, goal_cases)
           case k: (1 k)
           from d'(4)[OF this] guess u v by (elim exE) note uv=this
           def d' \<equiv> "{cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
@@ -10809,7 +10809,7 @@
             apply fact
             unfolding d'_def uv
             apply blast
-          proof (rule, goals)
+          proof (rule, goal_cases)
             case (1 i)
             then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
               by auto
@@ -10824,7 +10824,7 @@
             apply (rule setsum.reindex_nontrivial [unfolded o_def])
             apply (rule finite_imageI)
             apply (rule p')
-          proof goals
+          proof goal_cases
             case (1 l y)
             have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
               apply (subst(2) interior_inter)
@@ -10900,7 +10900,7 @@
           apply fact
           apply (rule finite_imageI[OF p'(1)])
           apply safe
-        proof goals
+        proof goal_cases
           case (2 i ia l a b)
           then have "ia \<inter> b = {}"
             unfolding p'alt image_iff Bex_def not_ex
@@ -11011,7 +11011,7 @@
             unfolding simple_image
             apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
             apply (rule d')
-          proof goals
+          proof goal_cases
             case (1 k y)
             from d'(4)[OF this(1)] d'(4)[OF this(2)]
             guess u1 v1 u2 v2 by (elim exE) note uv=this
@@ -11035,7 +11035,7 @@
             apply blast
             apply safe
             apply (rule_tac x=k in exI)
-          proof goals
+          proof goal_cases
             case (1 i k)
             from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
             have "interior (k \<inter> cbox u v) \<noteq> {}"
@@ -11085,7 +11085,7 @@
   show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
     apply (subst has_integral_alt')
     apply safe
-  proof goals
+  proof goal_cases
     case (1 a b)
     show ?case
       using f_int[of a b] by auto
@@ -11124,7 +11124,7 @@
         apply (rule *[rule_format])
         apply safe
         apply (rule d(2))
-      proof goals
+      proof goal_cases
         case 1
         have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
           apply (rule setsum_mono)
@@ -11251,7 +11251,7 @@
     apply (rule integrable_add)
     prefer 3
     apply safe
-  proof goals
+  proof goal_cases
     case (1 d)
     have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
       apply (drule division_ofD(4)[OF 1])
@@ -11310,12 +11310,12 @@
     apply (rule bounded_variation_absolutely_integrable[of _ "B * b"])
     apply (rule integrable_linear[OF _ assms(2)])
     apply safe
-  proof goals
+  proof goal_cases
     case (2 d)
     have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
       unfolding setsum_left_distrib
       apply (rule setsum_mono)
-    proof goals
+    proof goal_cases
       case (1 k)
       from division_ofD(4)[OF 2 this]
       guess u v by (elim exE) note uv=this
@@ -11455,7 +11455,7 @@
   show "f absolutely_integrable_on UNIV"
     apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"])
     apply safe
-  proof goals
+  proof goal_cases
     case (1 d)
     note d=this and d'=division_ofD[OF this]
     have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
@@ -11486,7 +11486,7 @@
     also have "\<dots> \<le> setsum (op \<bullet> (integral UNIV (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m))) Basis"
       apply (subst setsum.commute)
       apply (rule setsum_mono)
-    proof goals
+    proof goal_cases
       case (1 j)
       have *: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) integrable_on \<Union>d"
         using integrable_on_subdivision[OF d assms(2)] by auto
@@ -11541,7 +11541,7 @@
   show "f absolutely_integrable_on UNIV"
     apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
     apply safe
-  proof goals
+  proof goal_cases
     case d: (1 d)
     note d'=division_ofD[OF d]
     have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
@@ -11731,7 +11731,7 @@
       by (rule cInf_superset_mono) auto
     let ?S = "{f j x| j. m \<le> j}"
     show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
-    proof (rule LIMSEQ_I, goals)
+    proof (rule LIMSEQ_I, goal_cases)
       case r: (1 r)
 
       have "\<exists>y\<in>?S. y < Inf ?S + r"
@@ -11742,7 +11742,7 @@
       show ?case
         apply (rule_tac x=N in exI)
         apply safe
-      proof goals
+      proof goal_cases
         case (1 n)
         have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
           by arith
@@ -11802,7 +11802,7 @@
       by (rule cSup_subset_mono) auto
     let ?S = "{f j x| j. m \<le> j}"
     show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
-    proof (rule LIMSEQ_I, goals)
+    proof (rule LIMSEQ_I, goal_cases)
       case r: (1 r)
       have "\<exists>y\<in>?S. Sup ?S - r < y"
         by (subst less_cSup_iff[symmetric]) (auto simp: r \<open>x\<in>s\<close>)
@@ -11812,7 +11812,7 @@
       show ?case
         apply (rule_tac x=N in exI)
         apply safe
-      proof goals
+      proof goal_cases
         case (1 n)
         have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
           by arith
@@ -11856,7 +11856,7 @@
       by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)
 
     show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
-    proof (rule LIMSEQ_I, goals)
+    proof (rule LIMSEQ_I, goal_cases)
       case r: (1 r)
       then have "0<r/2"
         by auto
@@ -11904,7 +11904,7 @@
     show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
       by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
     show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
-    proof (rule LIMSEQ_I, goals)
+    proof (rule LIMSEQ_I, goal_cases)
       case r: (1 r)
       then have "0<r/2"
         by auto
@@ -11926,7 +11926,7 @@
 
   show "g integrable_on s" by fact
   show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
-  proof (rule LIMSEQ_I, goals)
+  proof (rule LIMSEQ_I, goal_cases)
     case r: (1 r)
     from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def]
     from LIMSEQ_D [OF dec2(2) r] guess N2 .. note N2=this[unfolded real_norm_def]
diff -r 8020249565fb -r 5976fe402824 src/HOL/Nominal/Examples/Pattern.thy
--- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -62,7 +62,7 @@
   by (simp add: supp_def Collect_disj_eq del: disj_not1)
 
 instance pat :: pt_name
-proof (default, goals)
+proof (default, goal_cases)
   case (1 x)
   show ?case by (induct x) simp_all
 next
@@ -74,7 +74,7 @@
 qed
 
 instance pat :: fs_name
-proof (default, goals)
+proof (default, goal_cases)
   case (1 x)
   show ?case by (induct x) (simp_all add: fin_supp)
 qed
diff -r 8020249565fb -r 5976fe402824 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -122,7 +122,7 @@
   "mark_out_aux n m [] = []"
   "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs"
   "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs"
-proof goals
+proof goal_cases
   case 1
   show ?case
     by (simp add: mark_out_aux_def)
diff -r 8020249565fb -r 5976fe402824 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -193,7 +193,7 @@
   assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
   shows "PiM I M = PiM J N"
   unfolding PiM_def
-proof (rule extend_measure_cong, goals)
+proof (rule extend_measure_cong, goal_cases)
   case 1
   show ?case using assms
     by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
diff -r 8020249565fb -r 5976fe402824 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -2078,7 +2078,7 @@
   "less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
 
 instance
-proof (standard, goals)
+proof (standard, goal_cases)
   case 1 then show ?case
     unfolding less_measure_def ..
 next
diff -r 8020249565fb -r 5976fe402824 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/ZF/Games.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -418,7 +418,7 @@
 proof (induct x rule: wf_induct[OF wf_option_of]) 
   case (1 "g")  
   show ?case
-  proof (auto, goals)
+  proof (auto, goal_cases)
     {case prems: (1 y) 
       from prems have "(y, g) \<in> option_of" by (auto)
       with 1 have "ge_game (y, y)" by auto
@@ -462,7 +462,7 @@
     proof (induct a rule: induct_game)
       case (1 a)
       show ?case
-      proof ((rule allI | rule impI)+, goals)
+      proof ((rule allI | rule impI)+, goal_cases)
         case prems: (1 x y z)
         show ?case
         proof -
@@ -543,7 +543,7 @@
 lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
 proof -
   have "H = zero_game \<longrightarrow> plus_game G H = G " for G H
-  proof (induct G H rule: plus_game.induct, rule impI, goals)
+  proof (induct G H rule: plus_game.induct, rule impI, goal_cases)
     case prems: (1 G H)
     note induct_hyp = this[simplified prems, simplified] and this
     show ?case
@@ -583,7 +583,7 @@
 lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
 proof -
   have "\<forall>F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)" for a
-  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+  proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
     case prems: (1 x F G H)
     let ?L = "plus_game (plus_game F G) H"
     let ?R = "plus_game F (plus_game G H)"
@@ -626,7 +626,7 @@
 qed
 
 lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
-proof (induct x rule: wf_induct[OF wf_option_of], goals)
+proof (induct x rule: wf_induct[OF wf_option_of], goal_cases)
   case prems: (1 x)
   then have ihyp: "eq_game (plus_game y (neg_game y)) zero_game" if "zin y (options x)" for y
     using that by (auto simp add: prems)
@@ -670,7 +670,7 @@
 lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
 proof -
   have "\<forall>x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)" for a
-  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+  proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
     case prems: (1 a x y z)
     note induct_hyp = prems(1)[rule_format, simplified prems(2)]
     { 
@@ -780,7 +780,7 @@
 lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
 proof -
   have "\<forall>x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
-  proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+  proof (induct a rule: induct_game, (rule impI | rule allI)+, goal_cases)
     case prems: (1 a x y)
     note ihyp = prems(1)[rule_format, simplified prems(2)]
     { fix xl
diff -r 8020249565fb -r 5976fe402824 src/HOL/ex/Tree23.thy
--- a/src/HOL/ex/Tree23.thy	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/HOL/ex/Tree23.thy	Sun Sep 13 20:20:16 2015 +0200
@@ -377,7 +377,7 @@
      done
   } note B = this
   show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
-  proof (induct k t arbitrary: n rule: del.induct, goals)
+  proof (induct k t arbitrary: n rule: del.induct, goal_cases)
     case (1 k n)
     thus "dfull n (del (Some k) Empty)" by simp
   next
diff -r 8020249565fb -r 5976fe402824 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Sep 13 16:50:12 2015 +0200
+++ b/src/Pure/Isar/method.ML	Sun Sep 13 20:20:16 2015 +0200
@@ -17,7 +17,7 @@
   val SIMPLE_METHOD: tactic -> method
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
-  val goals_tac: Proof.context -> string list -> cases_tactic
+  val goal_cases_tac: Proof.context -> string list -> cases_tactic
   val cheating: Proof.context -> bool -> method
   val intro: Proof.context -> thm list -> method
   val elim: Proof.context -> thm list -> method
@@ -130,7 +130,7 @@
 
 (* goals as cases *)
 
-fun goals_tac ctxt case_names st =
+fun goal_cases_tac ctxt case_names st =
   let
     val cases =
       (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
@@ -693,7 +693,7 @@
     "succeed after delay (in seconds)" #>
   setup @{binding "-"} (Scan.succeed (K insert_facts))
     "insert current facts, nothing else" #>
-  setup @{binding goals} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
+  setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
     METHOD_CASES (fn facts => fn st =>
       let
         val _ =
@@ -705,7 +705,7 @@
                 (* FIXME Seq.Error *)
                 error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
                   Position.here (Position.set_range (Token.range_of bad))));
-      in goals_tac ctxt (map Token.content_of names) st end)))
+      in goal_cases_tac ctxt (map Token.content_of names) st end)))
     "bind cases for goals" #>
   setup @{binding insert} (Attrib.thms >> (K o insert))
     "insert theorems, ignoring facts" #>