# HG changeset patch
# User nipkow
# Date 1442329753 -7200
# Node ID 16775cad1a5c8ed025f48c62037f8f473e560ace
# Parent  0b071f72f330d31824c6803d8c3765d174d4c1cb
goali -> i

diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -31,14 +31,15 @@
 lemma Some_le[simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
 by (cases u) auto
 
-instance proof
-  case goal1 show ?case by(rule less_option_def)
+instance
+proof (standard, goal_cases)
+  case 1 show ?case by(rule less_option_def)
 next
-  case goal2 show ?case by(cases x, simp_all)
+  case (2 x) show ?case by(cases x, simp_all)
 next
-  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, auto)
+  case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, auto)
 next
-  case goal4 thus ?case by(cases y, simp, cases x, auto)
+  case (4 x y) thus ?case by(cases y, simp, cases x, auto)
 qed
 
 end
@@ -63,14 +64,15 @@
 
 definition top_option where "\<top> = Some \<top>"
 
-instance proof
-  case goal4 show ?case by(cases a, simp_all add: top_option_def)
+instance
+proof (standard, goal_cases)
+  case (4 a) show ?case by(cases a, simp_all add: top_option_def)
 next
-  case goal1 thus ?case by(cases x, simp, cases y, simp_all)
+  case (1 x y) thus ?case by(cases x, simp, cases y, simp_all)
 next
-  case goal2 thus ?case by(cases y, simp, cases x, simp_all)
+  case (2 x y) thus ?case by(cases y, simp, cases x, simp_all)
 next
-  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+  case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
 qed
 
 end
@@ -85,8 +87,8 @@
 "\<bottom> = None"
 
 instance
-proof
-  case goal1 thus ?case by(auto simp: bot_option_def)
+proof (standard, goal_cases)
+  case 1 thus ?case by(auto simp: bot_option_def)
 qed
 
 end
diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -32,22 +32,22 @@
 definition "\<top> = Any"
 
 instance
-proof
-  case goal1 thus ?case by (rule less_const_def)
+proof (standard, goal_cases)
+  case 1 thus ?case by (rule less_const_def)
 next
-  case goal2 show ?case by (cases x) simp_all
+  case (2 x) show ?case by (cases x) simp_all
 next
-  case goal3 thus ?case by(cases z, cases y, cases x, simp_all)
+  case (3 x y z) thus ?case by(cases z, cases y, cases x, simp_all)
 next
-  case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
+  case (4 x y) thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
 next
-  case goal6 thus ?case by(cases x, cases y, simp_all)
+  case (6 x y) thus ?case by(cases x, cases y, simp_all)
 next
-  case goal5 thus ?case by(cases y, cases x, simp_all)
+  case (5 x y) thus ?case by(cases y, cases x, simp_all)
 next
-  case goal7 thus ?case by(cases z, cases y, cases x, simp_all)
+  case (7 x y z) thus ?case by(cases z, cases y, cases x, simp_all)
 next
-  case goal8 thus ?case by(simp add: top_const_def)
+  case 8 thus ?case by(simp add: top_const_def)
 qed
 
 end
@@ -55,16 +55,15 @@
 
 permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-proof
-  case goal1 thus ?case
+proof (standard, goal_cases)
+  case (1 a b) thus ?case
     by(cases a, cases b, simp, simp, cases b, simp, simp)
 next
-  case goal2 show ?case by(simp add: top_const_def)
+  case 2 show ?case by(simp add: top_const_def)
 next
-  case goal3 show ?case by simp
+  case 3 show ?case by simp
 next
-  case goal4 thus ?case
-    by(auto simp: plus_const_cases split: const.split)
+  case 4 thus ?case by(auto simp: plus_const_cases split: const.split)
 qed
 
 permanent_interpretation Abs_Int
@@ -123,9 +122,8 @@
 
 permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
-proof
-  case goal1 thus ?case
-    by(auto simp: plus_const_cases split: const.split)
+proof (standard, goal_cases)
+  case 1 thus ?case by(auto simp: plus_const_cases split: const.split)
 qed
 
 text{* Termination: *}
@@ -136,10 +134,10 @@
 permanent_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 and m = m_const and h = "1"
-proof
-  case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
+proof (standard, goal_cases)
+  case 1 thus ?case by(auto simp: m_const_def split: const.splits)
 next
-  case goal2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
+  case 2 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
 qed
 
 thm AI_Some_measure
diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -58,21 +58,21 @@
 definition top_parity where
 "\<top> = Either"
 
-text{* Now the instance proof. This time we take a lazy shortcut: we do not
-write out the proof obligations but use the @{text goali} primitive to refer
-to the assumptions of subgoal i and @{text "case?"} to refer to the
-conclusion of subgoal i. The class axioms are presented in the same order as
-in the class definition. Warning: this is brittle! *}
+text{* Now the instance proof. This time we take a shortcut with the help of
+proof method @{text goal_cases}: it creates cases 1 ... n for the subgoals
+1 ... n; in case i, i is also the name of the assumptions of subgoal i and
+@{text "case?"} refers to the conclusion of subgoal i.
+The class axioms are presented in the same order as in the class definition. *}
 
 instance
-proof
-  case goal1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
+proof (standard, goal_cases)
+  case 1 (*sup1*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
 next
-  case goal2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
+  case 2 (*sup2*) show ?case by(auto simp: less_eq_parity_def sup_parity_def)
 next
-  case goal3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
+  case 3 (*sup least*) thus ?case by(auto simp: less_eq_parity_def sup_parity_def)
 next
-  case goal4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
+  case 4 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
 qed
 
 end
@@ -104,21 +104,22 @@
 
 permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-proof txt{* of the locale axioms *}
-  fix a b :: parity
-  assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
-    by(auto simp: less_eq_parity_def)
-next txt{* The rest in the lazy, implicit way *}
-  case goal2 show ?case by(auto simp: top_parity_def)
+proof (standard, goal_cases) txt{* subgoals are the locale axioms *}
+  case 1 thus ?case by(auto simp: less_eq_parity_def)
 next
-  case goal3 show ?case by auto
+  case 2 show ?case by(auto simp: top_parity_def)
 next
-  txt{* Warning: this subproof refers to the names @{text a1} and @{text a2}
-  from the statement of the axiom. *}
-  case goal4 thus ?case
+  case 3 show ?case by auto
+next
+  case (4 _ a1 _ a2) thus ?case
     by (induction a1 a2 rule: plus_parity.induct) (auto simp add:mod_add_eq)
 qed
 
+text{* In case 4 we needed to refer to particular variables.
+Writing (i x y z) fixes the names of the variables in case i to be x, y and z
+in the left-to-right order in which the variables occur in the subgoal.
+Underscores are anonymous placeholders for variable names we don't care to fix. *}
+
 text{* Instantiating the abstract interpretation locale requires no more
 proofs (they happened in the instatiation above) but delivers the
 instantiated abstract interpreter which we call @{text AI_parity}: *}
@@ -156,8 +157,8 @@
 
 permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
-proof
-  case goal1 thus ?case
+proof (standard, goal_cases)
+  case (1 _ a1 _ a2) thus ?case
     by(induction a1 a2 rule: plus_parity.induct)
       (auto simp add:less_eq_parity_def)
 qed
@@ -168,10 +169,10 @@
 permanent_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 and m = m_parity and h = "1"
-proof
-  case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
+proof (standard, goal_cases)
+  case 1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
 next
-  case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
+  case 2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
 qed
 
 thm AI_Some_measure
diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -11,14 +11,14 @@
 definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
 
 instance
-proof
-  case goal1 show ?case by(rule less_prod_def)
+proof (standard, goal_cases)
+  case 1 show ?case by(rule less_prod_def)
 next
-  case goal2 show ?case by(simp add: less_eq_prod_def)
+  case 2 show ?case by(simp add: less_eq_prod_def)
 next
-  case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
+  case 3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
 next
-  case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
+  case 4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
 qed
 
 end
diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -104,22 +104,22 @@
 by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
 
 instance
-proof
-  case goal1 show ?case by (rule less_ivl_def)
+proof (standard, goal_cases)
+  case 1 show ?case by (rule less_ivl_def)
 next
-  case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
+  case 2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
 next
-  case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
+  case 3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
 next
-  case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
+  case 4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
 next
-  case goal5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
+  case 5 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
 next
-  case goal6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
+  case 6 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def is_empty_min_max)
 next
-  case goal7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def)
+  case 7 thus ?case by transfer (auto simp add: le_rep_def sup_rep_def)
 next
-  case goal8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
+  case 8 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
 qed
 
 end
@@ -132,8 +132,8 @@
 "equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
 
 instance
-proof
-  case goal1 show ?case by(simp add: equal_ivl_def eq_iff)
+proof (standard, goal_cases)
+  case 1 show ?case by(simp add: equal_ivl_def eq_iff)
 qed
 
 end
@@ -161,14 +161,14 @@
 definition "\<bottom> = empty_ivl"
 
 instance
-proof
-  case goal1 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
+proof (standard, goal_cases)
+  case 1 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
 next
-  case goal2 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
+  case 2 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
 next
-  case goal3 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
+  case 3 thus ?case by (simp add: \<gamma>_inf le_ivl_iff_subset)
 next
-  case goal4 show ?case
+  case 4 show ?case
     unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
 qed
 
@@ -304,14 +304,14 @@
 
 permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
-proof
-  case goal1 thus ?case by transfer (simp add: le_iff_subset)
+proof (standard, goal_cases)
+  case 1 thus ?case by transfer (simp add: le_iff_subset)
 next
-  case goal2 show ?case by transfer (simp add: \<gamma>_rep_def)
+  case 2 show ?case by transfer (simp add: \<gamma>_rep_def)
 next
-  case goal3 show ?case by transfer (simp add: \<gamma>_rep_def)
+  case 3 show ?case by transfer (simp add: \<gamma>_rep_def)
 next
-  case goal4 thus ?case
+  case 4 thus ?case
     apply transfer
     apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
     by(auto simp: empty_rep_def is_empty_rep_def)
@@ -321,26 +321,26 @@
 permanent_interpretation Val_lattice_gamma
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 defining aval_ivl = aval'
-proof
-  case goal1 show ?case by(simp add: \<gamma>_inf)
+proof (standard, goal_cases)
+  case 1 show ?case by(simp add: \<gamma>_inf)
 next
-  case goal2 show ?case unfolding bot_ivl_def by transfer simp
+  case 2 show ?case unfolding bot_ivl_def by transfer simp
 qed
 
 permanent_interpretation Val_inv
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-proof
-  case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
+proof (standard, goal_cases)
+  case 1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
 next
-  case goal2 thus ?case
+  case (2 _ _ _ _ _ i1 i2) thus ?case
     unfolding inv_plus_ivl_def minus_ivl_def
     apply(clarsimp simp add: \<gamma>_inf)
     using gamma_plus'[of "i1+i2" _ "-i1"] gamma_plus'[of "i1+i2" _ "-i2"]
     by(simp add:  \<gamma>_uminus)
 next
-  case goal3 thus ?case
+  case (3 i1 i2) thus ?case
     unfolding inv_less_ivl_def minus_ivl_def one_extended_def
     apply(clarsimp simp add: \<gamma>_inf split: if_splits)
     using gamma_plus'[of "i1+1" _ "-1"] gamma_plus'[of "i2 - 1" _ "1"]
@@ -388,14 +388,14 @@
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
-proof
-  case goal1 thus ?case by (rule mono_plus_ivl)
+proof (standard, goal_cases)
+  case 1 thus ?case by (rule mono_plus_ivl)
 next
-  case goal2 thus ?case
+  case 2 thus ?case
     unfolding inv_plus_ivl_def minus_ivl_def less_eq_prod_def
     by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_minus_ivl)
 next
-  case goal3 thus ?case
+  case 3 thus ?case
     unfolding less_eq_prod_def inv_less_ivl_def minus_ivl_def
     by (auto simp: le_infI1 le_infI2 mono_plus_ivl mono_above mono_below)
 qed
diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -63,18 +63,14 @@
 by(auto simp: eq_st_def)
 
 instance
-proof
-  case goal1 thus ?case
-    by transfer (simp add: less_eq_st_rep_iff widen1)
+proof (standard, goal_cases)
+  case 1 thus ?case by transfer (simp add: less_eq_st_rep_iff widen1)
 next
-  case goal2 thus ?case
-    by transfer (simp add: less_eq_st_rep_iff widen2)
+  case 2 thus ?case by transfer (simp add: less_eq_st_rep_iff widen2)
 next
-  case goal3 thus ?case
-    by transfer (simp add: less_eq_st_rep_iff narrow1)
+  case 3 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow1)
 next
-  case goal4 thus ?case
-    by transfer (simp add: less_eq_st_rep_iff narrow2)
+  case 4 thus ?case by transfer (simp add: less_eq_st_rep_iff narrow2)
 qed
 
 end
@@ -94,17 +90,17 @@
 "(Some x) \<triangle> (Some y) = Some(x \<triangle> y)"
 
 instance
-proof
-  case goal1 thus ?case
+proof (standard, goal_cases)
+  case (1 x y) thus ?case
     by(induct x y rule: widen_option.induct)(simp_all add: widen1)
 next
-  case goal2 thus ?case
+  case (2 x y) thus ?case
     by(induct x y rule: widen_option.induct)(simp_all add: widen2)
 next
-  case goal3 thus ?case
+  case (3 x y) thus ?case
     by(induct x y rule: narrow_option.induct) (simp_all add: narrow1)
 next
-  case goal4 thus ?case
+  case (4 y x) thus ?case
     by(induct x y rule: narrow_option.induct) (simp_all add: narrow2)
 qed
 
@@ -550,14 +546,14 @@
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
 and m = m_ivl and n = n_ivl and h = 3
-proof
-  case goal2 thus ?case by(rule m_ivl_anti_mono)
+proof (standard, goal_cases)
+  case 2 thus ?case by(rule m_ivl_anti_mono)
 next
-  case goal1 thus ?case by(rule m_ivl_height)
+  case 1 thus ?case by(rule m_ivl_height)
 next
-  case goal3 thus ?case by(rule m_ivl_widen)
+  case 3 thus ?case by(rule m_ivl_widen)
 next
-  case goal4 from goal4(2) show ?case by(rule n_ivl_narrow)
+  case 4 from 4(2) show ?case by(rule n_ivl_narrow)
   -- "note that the first assms is unnecessary for intervals"
 qed
 
diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -66,15 +66,14 @@
 definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
 
 instance
-proof
-  case goal1 show ?case by(rule less_st_def)
-next
-  case goal2 show ?case by transfer (auto simp: less_eq_st_rep_def)
+proof (standard, goal_cases)
+  case 1 show ?case by(rule less_st_def)
 next
-  case goal3 thus ?case
-    by transfer (metis less_eq_st_rep_iff order_trans)
+  case 2 show ?case by transfer (auto simp: less_eq_st_rep_def)
 next
-  case goal4 thus ?case
+  case 3 thus ?case by transfer (metis less_eq_st_rep_iff order_trans)
+next
+  case 4 thus ?case
     by transfer (metis less_eq_st_rep_iff eq_st_def fun_eq_iff antisym)
 qed
 
@@ -105,15 +104,14 @@
 lift_definition top_st :: "'a st" is "[]" .
 
 instance
-proof
-  case goal1 show ?case by transfer (simp add:less_eq_st_rep_iff)
-next
-  case goal2 show ?case by transfer (simp add:less_eq_st_rep_iff)
+proof (standard, goal_cases)
+  case 1 show ?case by transfer (simp add:less_eq_st_rep_iff)
 next
-  case goal3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
+  case 2 show ?case by transfer (simp add:less_eq_st_rep_iff)
 next
-  case goal4 show ?case
-    by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
+  case 3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
+next
+  case 4 show ?case by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
 qed
 
 end
diff -r 0b071f72f330 -r 16775cad1a5c src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Tue Sep 15 11:18:25 2015 +0200
+++ b/src/HOL/IMP/Collecting.thy	Tue Sep 15 17:09:13 2015 +0200
@@ -45,14 +45,14 @@
 "less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
 
 instance
-proof
-  case goal1 show ?case by(simp add: less_acom_def)
+proof (standard, goal_cases)
+  case 1 show ?case by(simp add: less_acom_def)
 next
-  case goal2 thus ?case by(auto simp: less_eq_acom_def)
+  case 2 thus ?case by(auto simp: less_eq_acom_def)
 next
-  case goal3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
+  case 3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
 next
-  case goal4 thus ?case
+  case 4 thus ?case
     by(fastforce simp: le_antisym less_eq_acom_def size_annos
          eq_acom_iff_strip_anno)
 qed
@@ -97,14 +97,14 @@
 
 permanent_interpretation
   Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
-proof
-  case goal1 thus ?case
+proof (standard, goal_cases)
+  case 1 thus ?case
     by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_lower)
 next
-  case goal2 thus ?case
+  case 2 thus ?case
     by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_greatest)
 next
-  case goal3 thus ?case by(auto simp: Inf_acom_def)
+  case 3 thus ?case by(auto simp: Inf_acom_def)
 qed