# HG changeset patch
# User wenzelm
# Date 1181685701 -7200
# Node ID 50c5b0912a0ce2cb51dbb55a00928ffb638ad2f9
# Parent  23a8345f89f57f0328dcf303f4d04ac83c46ed1f
tuned proofs: avoid implicit prems;

diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -185,13 +185,13 @@
 
 lemma (in additive_subgroup) is_additive_subgroup:
   shows "additive_subgroup H G"
-by -
+by fact
 
 lemma additive_subgroupI:
   includes struct G
   assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "additive_subgroup H G"
-by (rule additive_subgroup.intro)
+by (rule additive_subgroup.intro) (rule a_subgroup)
 
 lemma (in additive_subgroup) a_subset:
      "H \<subseteq> carrier G"
@@ -225,7 +225,7 @@
 
 lemma (in abelian_subgroup) is_abelian_subgroup:
   shows "abelian_subgroup H G"
-by -
+by fact
 
 lemma abelian_subgroupI:
   assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
@@ -328,14 +328,22 @@
 lemma (in abelian_group) a_l_repr_imp_subset:
   assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "y <+ H \<subseteq> x <+ H"
-by (rule group.l_repr_imp_subset [OF a_group,
+apply (rule group.l_repr_imp_subset [OF a_group,
     folded a_l_coset_def, simplified monoid_record_simps])
+apply (rule y)
+apply (rule x)
+apply (rule sb)
+done
 
 lemma (in abelian_group) a_l_repr_independence:
   assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   shows "x <+ H = y <+ H"
-by (rule group.l_repr_independence [OF a_group,
+apply (rule group.l_repr_independence [OF a_group,
     folded a_l_coset_def, simplified monoid_record_simps])
+apply (rule y)
+apply (rule x)
+apply (rule sb)
+done
 
 lemma (in abelian_group) setadd_subset_G:
      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
@@ -350,7 +358,7 @@
   assumes x:     "x \<in> carrier G"
   shows "a_set_inv (H +> x) = H +> (\<ominus> x)" 
 by (rule normal.rcos_inv [OF a_normal,
-    folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps])
+  folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)
 
 lemma (in abelian_group) a_setmult_rcos_assoc:
      "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
@@ -388,7 +396,7 @@
   assumes a: "a \<in> carrier G"
   shows "a <+ H = racong H `` {a}"
 by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
-    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
+    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)
 
 lemma (in abelian_subgroup) a_rcos_equation:
   shows
@@ -531,7 +539,11 @@
   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
                                   (| carrier = carrier H, mult = add H, one = zero H |) h"
   shows "abelian_group_hom G H h"
-by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
+  apply (rule G.abelian_group_axioms)
+ apply (rule H.abelian_group_axioms)
+apply (rule a_group_hom)
+done
 
 lemma (in abelian_group_hom) is_abelian_group_hom:
   "abelian_group_hom G H h"
@@ -588,13 +600,13 @@
   assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
   shows "X \<noteq> {}"
 by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
-    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
 
 lemma (in abelian_group_hom) FactGroup_contents_mem:
   assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
   shows "contents (h`X) \<in> carrier H"
 by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
-    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
 
 lemma (in abelian_group_hom) A_FactGroup_hom:
      "(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
@@ -613,7 +625,7 @@
   assumes h: "h ` carrier G = carrier H"
   shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
 by (rule group_hom.FactGroup_onto[OF a_group_hom,
-    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
 
 text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
@@ -634,7 +646,7 @@
   assumes hH: "h \<in> H"
   shows "h \<in> carrier G"
 by (rule subgroup.mem_carrier [OF a_subgroup,
-    simplified monoid_record_simps])
+    simplified monoid_record_simps]) (rule hH)
 
 
 subsection {* Lemmas for Right Cosets *}
@@ -644,31 +656,33 @@
       and a': "a' \<in> H +> a"
   shows "a' \<in> carrier G"
 by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
-    folded a_r_coset_def, simplified monoid_record_simps])
+    folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')
 
 lemma (in abelian_subgroup) a_rcos_const:
   assumes hH: "h \<in> H"
   shows "H +> h = H"
 by (rule subgroup.rcos_const [OF a_subgroup a_group,
-    folded a_r_coset_def, simplified monoid_record_simps])
+    folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)
 
 lemma (in abelian_subgroup) a_rcos_module_imp:
   assumes xcarr: "x \<in> carrier G"
       and x'cos: "x' \<in> H +> x"
   shows "(x' \<oplus> \<ominus>x) \<in> H"
 by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
-    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
+    folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)
 
 lemma (in abelian_subgroup) a_rcos_module_rev:
-  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
-      and xixH: "(x' \<oplus> \<ominus>x) \<in> H"
+  assumes "x \<in> carrier G" "x' \<in> carrier G"
+      and "(x' \<oplus> \<ominus>x) \<in> H"
   shows "x' \<in> H +> x"
+using assms
 by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
 
 lemma (in abelian_subgroup) a_rcos_module:
-  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
+  assumes "x \<in> carrier G" "x' \<in> carrier G"
   shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
+using assms
 by (rule subgroup.rcos_module [OF a_subgroup a_group,
     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
 
@@ -679,10 +693,10 @@
   shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
 proof -
   from carr
-      have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
-  from this and carr
-      show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
-      by (simp add: minus_eq)
+  have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
+  with carr
+  show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
+    by (simp add: minus_eq)
 qed
 
 lemma (in abelian_subgroup) a_repr_independence':
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Coset.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -107,13 +107,17 @@
                     subgroup.one_closed)
 done
 
-text {* Opposite of @{thm [locale=group,source] "repr_independence"} *}
+text (in group) {* Opposite of @{thm [source] "repr_independence"} *}
 lemma (in group) repr_independenceD:
   includes subgroup H G
   assumes ycarr: "y \<in> carrier G"
       and repr:  "H #> x = H #> y"
   shows "y \<in> H #> x"
-  by (subst repr, intro rcos_self)
+  apply (subst repr)
+  apply (intro rcos_self)
+   apply (rule ycarr)
+   apply (rule is_subgroup)
+  done
 
 text {* Elements of a right coset are in the carrier *}
 lemma (in subgroup) elemrcos_carrier:
@@ -819,8 +823,8 @@
   includes group G
   shows "H \<in> rcosets H"
 proof -
-  have "H #> \<one> = H"
-    by (rule coset_join2, auto)
+  from _ `subgroup H G` have "H #> \<one> = H"
+    by (rule coset_join2) auto
   then show ?thesis
     by (auto simp add: RCOSETS_def)
 qed
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -263,9 +263,9 @@
 
 lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x"
 proof -
-  assume D: "x \<in> D"
-  have "x \<cdot> e = x" by (rule ident)
-  with D show ?thesis by (simp add: commute)
+  assume "x \<in> D"
+  then have "x \<cdot> e = x" by (rule ident)
+  with `x \<in> D` show ?thesis by (simp add: commute)
 qed
 
 lemma (in ACeD) foldD_Un_Int:
@@ -424,9 +424,9 @@
       then have "finprod G f A = finprod G f (insert x B)" by simp
       also from insert have "... = f x \<otimes> finprod G f B"
       proof (intro finprod_insert)
-	show "finite B" .
+	show "finite B" by fact
       next
-	show "x ~: B" .
+	show "x ~: B" by fact
       next
 	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
 	  "g \<in> insert x B \<rightarrow> carrier G"
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -195,7 +195,7 @@
   assumes Units: "carrier G <= Units G"
 
 
-lemma (in group) is_group: "group G" .
+lemma (in group) is_group: "group G" by fact
 
 theorem groupI:
   fixes G (structure)
@@ -383,7 +383,7 @@
     and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
 
 lemma (in subgroup) is_subgroup:
-  "subgroup H G" .
+  "subgroup H G" by fact
 
 declare (in subgroup) group.intro [intro]
 
@@ -694,7 +694,7 @@
 
 lemma (in group) subgroup_imp_group:
   "subgroup H G ==> group (G(| carrier := H |))"
-  by (rule subgroup.subgroup_is_group)
+  by (erule subgroup.subgroup_is_group) (rule `group G`)
 
 lemma (in group) is_monoid [intro, simp]:
   "monoid G"
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -25,7 +25,7 @@
 
 lemma (in ideal) is_ideal:
   "ideal I R"
-by -
+by fact
 
 lemma idealI:
   includes ring
@@ -50,7 +50,7 @@
 
 lemma (in principalideal) is_principalideal:
   shows "principalideal I R"
-by -
+by fact
 
 lemma principalidealI:
   includes ideal
@@ -85,7 +85,7 @@
 
 lemma (in primeideal) is_primeideal:
  shows "primeideal I R"
-by -
+by fact
 
 lemma primeidealI:
   includes ideal
@@ -166,7 +166,7 @@
 lemma (in ideal) Icarr:
   assumes iI: "i \<in> I"
   shows "i \<in> carrier R"
-by (rule a_Hcarr)
+using iI by (rule a_Hcarr)
 
 
 subsection {* Intersection of Ideals *}
@@ -361,7 +361,7 @@
   shows "(Idl H \<subseteq> I) = (H \<subseteq> I)"
 proof
   assume a: "Idl H \<subseteq> I"
-  have "H \<subseteq> Idl H" by (rule genideal_self)
+  from Hcarr have "H \<subseteq> Idl H" by (rule genideal_self)
   from this and a
       show "H \<subseteq> I" by simp
 next
@@ -504,8 +504,11 @@
   assumes aJ: "a \<in> J"
   shows "PIdl a \<subseteq> J"
 unfolding cgenideal_def
-by (rule, clarify, rule I_l_closed)
-
+apply rule
+apply clarify
+using aJ
+apply (erule I_l_closed)
+done
 
 lemma (in cring) cgenideal_eq_genideal:
   assumes icarr: "i \<in> carrier R"
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -265,7 +265,7 @@
 	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
           with y L show ?thesis by blast
 	qed
-      qed (rule Upper_closed [THEN subsetD])
+      qed (rule Upper_closed [THEN subsetD, OF y])
     next
       from L show "insert x A \<subseteq> carrier L" by simp
       from least_s show "s \<in> carrier L" by simp
@@ -307,13 +307,13 @@
             assume "z \<in> {x}"
             with y L show ?thesis by blast
           qed
-        qed (rule Upper_closed [THEN subsetD])
+        qed (rule Upper_closed [THEN subsetD, OF y])
       next
         from L show "insert x A \<subseteq> carrier L" by simp
         from least_s show "s \<in> carrier L" by simp
       qed
-    qed
-  qed
+    qed (rule least_l)
+  qed (rule P)
 qed
 
 lemma (in lattice) finite_sup_least:
@@ -375,12 +375,12 @@
 
 lemma (in lattice) join_le:
   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
-    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   shows "x \<squnion> y \<sqsubseteq> z"
-proof (rule joinI)
+proof (rule joinI [OF _ x y])
   fix s
   assume "least L s (Upper L {x, y})"
-  with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
+  with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
 qed
 
 lemma (in lattice) join_assoc_lemma:
@@ -491,7 +491,7 @@
           assume "z \<in> {x}"
           with y L show ?thesis by blast
 	qed
-      qed (rule Lower_closed [THEN subsetD])
+      qed (rule Lower_closed [THEN subsetD, OF y])
     next
       from L show "insert x A \<subseteq> carrier L" by simp
       from greatest_i show "i \<in> carrier L" by simp
@@ -533,13 +533,13 @@
             assume "z \<in> {x}"
             with y L show ?thesis by blast
 	  qed
-        qed (rule Lower_closed [THEN subsetD])
+        qed (rule Lower_closed [THEN subsetD, OF y])
       next
         from L show "insert x A \<subseteq> carrier L" by simp
         from greatest_i show "i \<in> carrier L" by simp
       qed
-    qed
-  qed
+    qed (rule greatest_g)
+  qed (rule P)
 qed
 
 lemma (in lattice) finite_inf_greatest:
@@ -603,12 +603,12 @@
 
 lemma (in lattice) meet_le:
   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
-    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   shows "z \<sqsubseteq> x \<sqinter> y"
-proof (rule meetI)
+proof (rule meetI [OF _ x y])
   fix i
   assume "greatest L i (Lower L {x, y})"
-  with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
+  with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
 qed
 
 lemma (in lattice) meet_assoc_lemma:
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/QuotRing.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -247,23 +247,23 @@
   assume "\<zero>\<^bsub>R Quot I\<^esub> = \<one>\<^bsub>R Quot I\<^esub>"
   hence II1: "I = I +> \<one>" by (simp add: FactRing_def)
   from a_rcos_self[OF one_closed]
-      have "\<one> \<in> I" by (simp add: II1[symmetric])
+  have "\<one> \<in> I" by (simp add: II1[symmetric])
   hence "I = carrier R" by (rule one_imp_carrier)
   from this and I_notcarr
-      show "False" by simp
+  show "False" by simp
 next
   --{* Existence of Inverse *}
   fix a
   assume IanI: "I +> a \<noteq> I"
-     and acarr: "a \<in> carrier R"
+    and acarr: "a \<in> carrier R"
 
   --{* Helper ideal @{text "J"} *}
   def J \<equiv> "(carrier R #> a) <+> I :: 'a set"
   have idealJ: "ideal J R"
-      apply (unfold J_def, rule add_ideals)
-      apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
-      apply (rule is_ideal)
-      done
+    apply (unfold J_def, rule add_ideals)
+     apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr)
+    apply (rule is_ideal)
+    done
 
   --{* Showing @{term "J"} not smaller than @{term "I"} *}
   have IinJ: "I \<subseteq> J"
@@ -275,7 +275,7 @@
     have "x = \<zero> \<otimes> a \<oplus> x" by algebra
 
     from Zcarr and xI and this
-        show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
+    show "\<exists>xa\<in>carrier R. \<exists>k\<in>I. x = xa \<otimes> a \<oplus> k" by fast
   qed
 
   --{* Showing @{term "J \<noteq> I"} *}
@@ -284,57 +284,58 @@
     assume "a \<in> I"
     hence "I +> a = I" by (rule a_rcos_const)
     from this and IanI
-        show "False" by simp
+    show "False" by simp
   qed
 
   have aJ: "a \<in> J"
   proof (simp add: J_def r_coset_def set_add_defs)
     from acarr
-        have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
+    have "a = \<one> \<otimes> a \<oplus> \<zero>" by algebra
     from one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] and this
-        show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
+    show "\<exists>x\<in>carrier R. \<exists>k\<in>I. a = x \<otimes> a \<oplus> k" by fast
   qed
 
   from aJ and anI
-      have JnI: "J \<noteq> I" by fast
+  have JnI: "J \<noteq> I" by fast
 
   --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *}
   from idealJ and IinJ
-      have "J = I \<or> J = carrier R"
+  have "J = I \<or> J = carrier R"
   proof (rule I_maximal, unfold J_def)
     have "carrier R #> a \<subseteq> carrier R"
-	  by (rule r_coset_subset_G) fast
+      using subset_refl acarr
+      by (rule r_coset_subset_G)
     from this and a_subset
-        show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed)
+    show "carrier R #> a <+> I \<subseteq> carrier R" by (rule set_add_closed)
   qed
 
   from this and JnI
-      have Jcarr: "J = carrier R" by simp
+  have Jcarr: "J = carrier R" by simp
 
   --{* Calculating an inverse for @{term "a"} *}
   from one_closed[folded Jcarr]
-      have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
-      by (simp add: J_def r_coset_def set_add_defs)
+  have "\<exists>r\<in>carrier R. \<exists>i\<in>I. \<one> = r \<otimes> a \<oplus> i"
+    by (simp add: J_def r_coset_def set_add_defs)
   from this
-     obtain r i
-       where rcarr: "r \<in> carrier R"
-       and iI: "i \<in> I"
-       and one: "\<one> = r \<otimes> a \<oplus> i"
-     by fast
+  obtain r i
+    where rcarr: "r \<in> carrier R"
+      and iI: "i \<in> I"
+      and one: "\<one> = r \<otimes> a \<oplus> i"
+    by fast
   from one and rcarr and acarr and iI[THEN a_Hcarr]
-      have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
+  have rai1: "a \<otimes> r = \<ominus>i \<oplus> \<one>" by algebra
 
   --{* Lifting to cosets *}
   from iI
-      have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
-      by (intro a_rcosI, simp, intro a_subset, simp)
+  have "\<ominus>i \<oplus> \<one> \<in> I +> \<one>"
+    by (intro a_rcosI, simp, intro a_subset, simp)
   from this and rai1
-      have "a \<otimes> r \<in> I +> \<one>" by simp
+  have "a \<otimes> r \<in> I +> \<one>" by simp
   from this have "I +> \<one> = I +> a \<otimes> r"
-      by (rule a_repr_independence, simp) (rule a_subgroup)
+    by (rule a_repr_independence, simp) (rule a_subgroup)
 
   from rcarr and this[symmetric]
-      show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
+  show "\<exists>r\<in>carrier R. I +> a \<otimes> r = I +> \<one>" by fast
 qed
 
 end
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/Ring.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -249,8 +249,11 @@
   fixes A
   assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   shows "finsum G f A \<in> carrier G"
-  by (rule comm_monoid.finprod_closed [OF a_comm_monoid,
+  apply (rule comm_monoid.finprod_closed [OF a_comm_monoid,
     folded finsum_def, simplified monoid_record_simps])
+   apply (rule fin)
+  apply (rule f)
+  done
 
 lemma (in abelian_monoid) finsum_Un_Int:
   "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
@@ -359,7 +362,7 @@
 
 lemma (in ring) is_ring:
   "ring R"
-  .
+  by fact
 
 lemmas ring_record_simps = monoid_record_simps ring.simps
 
@@ -370,34 +373,34 @@
     and l_distr: "!!x y z. [| x \<in> carrier R; y \<in> carrier R; z \<in> carrier R |]
       ==> (x \<oplus> y) \<otimes> z = x \<otimes> z \<oplus> y \<otimes> z"
   shows "cring R"
-  proof (intro cring.intro ring.intro)
-    show "ring_axioms R"
+proof (intro cring.intro ring.intro)
+  show "ring_axioms R"
     -- {* Right-distributivity follows from left-distributivity and
           commutativity. *}
-    proof (rule ring_axioms.intro)
-      fix x y z
-      assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
-      note [simp]= comm_monoid.axioms [OF comm_monoid]
-        abelian_group.axioms [OF abelian_group]
-        abelian_monoid.a_closed
+  proof (rule ring_axioms.intro)
+    fix x y z
+    assume R: "x \<in> carrier R" "y \<in> carrier R" "z \<in> carrier R"
+    note [simp] = comm_monoid.axioms [OF comm_monoid]
+      abelian_group.axioms [OF abelian_group]
+      abelian_monoid.a_closed
         
-      from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
-        by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
-      also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
-      also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
-        by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
-      finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
-    qed
-  qed (auto intro: cring.intro
-      abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
+    from R have "z \<otimes> (x \<oplus> y) = (x \<oplus> y) \<otimes> z"
+      by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
+    also from R have "... = x \<otimes> z \<oplus> y \<otimes> z" by (simp add: l_distr)
+    also from R have "... = z \<otimes> x \<oplus> z \<otimes> y"
+      by (simp add: comm_monoid.m_comm [OF comm_monoid.intro])
+    finally show "z \<otimes> (x \<oplus> y) = z \<otimes> x \<oplus> z \<otimes> y" .
+  qed (rule l_distr)
+qed (auto intro: cring.intro
+  abelian_group.axioms comm_monoid.axioms ring_axioms.intro prems)
 
 lemma (in cring) is_comm_monoid:
   "comm_monoid R"
   by (auto intro!: comm_monoidI m_assoc m_comm)
 
 lemma (in cring) is_cring:
-  "cring R"
-  .
+  "cring R" by fact
+
 
 subsubsection {* Normaliser for Rings *}
 
@@ -647,7 +650,7 @@
     have "b = \<zero>" .
     thus "a = \<zero> \<or> b = \<zero>" by simp
   qed
-qed
+qed (rule field_Units)
 
 text {* Another variant to show that something is a field *}
 lemma (in cring) cring_fieldI2:
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -34,7 +34,7 @@
 lemma (in ring_hom_ring) is_ring_hom_ring:
   includes struct R + struct S
   shows "ring_hom_ring R S h"
-by -
+by fact
 
 lemma ring_hom_ringI:
   includes ring R + ring S
@@ -51,9 +51,13 @@
 
 lemma ring_hom_ringI2:
   includes ring R + ring S
-  assumes "h \<in> ring_hom R S"
+  assumes h: "h \<in> ring_hom R S"
   shows "ring_hom_ring R S h"
-by (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro)
+apply (rule R.is_ring)
+apply (rule S.is_ring)
+apply (rule h)
+done
 
 lemma ring_hom_ringI3:
   includes abelian_group_hom R S + ring R + ring S 
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -306,7 +306,7 @@
     next
       case (Suc k)
       then have "k <= n" by arith
-      then have "?eq k" by (rule Suc)
+      from this R have "?eq k" by (rule Suc)
       with R show ?case
         by (simp cong: finsum_cong
              add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
@@ -633,14 +633,14 @@
 *)
 
 lemma (in UP_cring) deg_aboveD:
-  "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
+  assumes "deg R p < m" and "p \<in> carrier P"
+  shows "coeff P p m = \<zero>"
 proof -
-  assume R: "p \<in> carrier P" and "deg R p < m"
-  from R obtain n where "bound \<zero> n (coeff P p)"
+  from `p \<in> carrier P` obtain n where "bound \<zero> n (coeff P p)"
     by (auto simp add: UP_def P_def)
   then have "bound \<zero> (deg R p) (coeff P p)"
     by (auto simp: deg_def P_def dest: LeastI)
-  then show ?thesis ..
+  from this and `deg R p < m` show ?thesis ..
 qed
 
 lemma (in UP_cring) deg_belowI:
@@ -672,7 +672,7 @@
     then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
       by (unfold bound_def) fast
     then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
-    then show ?thesis by auto
+    then show ?thesis by (auto intro: that)
   qed
   with deg_belowI R have "deg R p = m" by fastsimp
   with m_coeff show ?thesis by simp
@@ -689,7 +689,7 @@
     with nonzero show ?thesis by contradiction
   qed
   then obtain m where coeff: "coeff P p m ~= \<zero>" ..
-  then have "m <= deg R p" by (rule deg_belowI)
+  from this and R have "m <= deg R p" by (rule deg_belowI)
   then have "m = 0" by (simp add: deg)
   with coeff show ?thesis by simp
 qed
@@ -773,7 +773,7 @@
   shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
 proof (rule le_anti_sym)
   show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
-    by (rule deg_smult_ring)
+    using R by (rule deg_smult_ring)
 next
   show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^bsub>P\<^esub> p)"
   proof (cases "a = \<zero>")
@@ -805,7 +805,7 @@
   deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
 proof (rule le_anti_sym)
   assume "p \<in> carrier P" " q \<in> carrier P"
-  show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring)
+  then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring)
 next
   let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
   assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>"
@@ -884,7 +884,7 @@
   also have "... = finsum P ?s {..deg R p}"
     by (simp cong: P.finsum_cong add: P.finsum_Un_disjoint ivl_disj_int_one
       deg_aboveD R Pi_def)
-  also have "... = p" by (rule up_repr)
+  also have "... = p" using R by (rule up_repr)
   finally show ?thesis .
 qed
 
@@ -1301,6 +1301,7 @@
     and "cring S"
     and "h \<in> ring_hom R S"
   shows "UP_pre_univ_prop R S h"
+  using assms
   by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
     ring_hom_cring_axioms.intro UP_cring.intro)
 
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -439,11 +439,11 @@
 by (unfold deg_def) (fast intro: Least_le)
 
 lemma deg_aboveD:
-  assumes prem: "deg p < m" shows "coeff p m = 0"
+  assumes "deg p < m" shows "coeff p m = 0"
 proof -
   obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain)
   then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI)
-  then show "coeff p m = 0" by (rule boundD)
+  then show "coeff p m = 0" using `deg p < m` by (rule boundD)
 qed
 
 lemma deg_belowI:
@@ -470,7 +470,7 @@
     then have "EX m. deg p - 1 < m & coeff p m ~= 0"
       by (unfold bound_def) fast
     then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus)
-    then show ?thesis by auto 
+    then show ?thesis by (auto intro: that)
   qed
   with deg_belowI have "deg p = m" by fastsimp
   with m_coeff show ?thesis by simp
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/AxSound.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -6,8 +6,6 @@
           statements
        *}
 
-
-
 theory AxSound imports AxSem begin
 
 section "validity"
@@ -101,7 +99,7 @@
 apply (fast intro: triple_valid2_Suc)
 done
 
-lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)";
+lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)"
 oops
 
 
@@ -131,8 +129,8 @@
       qed
     next
       case (Suc m)
-      have hyp: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t".
-      have prem: "\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t" .
+      note hyp = `\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t`
+      note prem = `\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t`
       show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>Suc m\<Colon>t"
       proof -
 	{
@@ -357,8 +355,9 @@
     by (simp add: ax_valids2_def triple_valid2_def2)
 next
   case (insert A t ts)
-  have valid_t: "G,A|\<Turnstile>\<Colon>{t}" . 
-  moreover have valid_ts: "G,A|\<Turnstile>\<Colon>ts" .
+  note valid_t = `G,A|\<Turnstile>\<Colon>{t}`
+  moreover
+  note valid_ts = `G,A|\<Turnstile>\<Colon>ts`
   {
     fix n assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
     have "G\<Turnstile>n\<Colon>t" and "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
@@ -376,21 +375,21 @@
     by (unfold ax_valids2_def) blast
 next
   case (asm ts A)
-  have "ts \<subseteq> A" .
-  then show "G,A|\<Turnstile>\<Colon>ts"
+  from `ts \<subseteq> A`
+  show "G,A|\<Turnstile>\<Colon>ts"
     by (auto simp add: ax_valids2_def triple_valid2_def)
 next
   case (weaken A ts' ts)
-  have "G,A|\<Turnstile>\<Colon>ts'" .
-  moreover have "ts \<subseteq> ts'" .
+  note `G,A|\<Turnstile>\<Colon>ts'`
+  moreover note `ts \<subseteq> ts'`
   ultimately show "G,A|\<Turnstile>\<Colon>ts"
     by (unfold ax_valids2_def triple_valid2_def) blast
 next
   case (conseq P A t Q)
-  have con: "\<forall>Y s Z. P Y s Z \<longrightarrow> 
+  note con = `\<forall>Y s Z. P Y s Z \<longrightarrow> 
               (\<exists>P' Q'.
                   (G,A\<turnstile>{P'} t\<succ> {Q'} \<and> G,A|\<Turnstile>\<Colon>{ {P'} t\<succ> {Q'} }) \<and>
-                  (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))".
+                  (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))`
   show "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
   proof (rule validI)
     fix n s0 L accC T C v s1 Y Z
@@ -475,8 +474,8 @@
   qed
 next
   case (FVar A P statDeclC Q e stat fn R accC)
-  have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }" .
-  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }" .
+  note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }`
+  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC,statDeclC,stat}e..fn=\<succ> {R} }"
   proof (rule valid_var_NormalI)
     fix n s0 L accC' T V vf s3 Y Z
@@ -536,8 +535,8 @@
 	  from eval_init 
 	  have "(dom (locals (store s0))) \<subseteq> (dom (locals (store s1)))"
 	    by (rule dom_locals_evaln_mono_elim)
-	  with da_e show ?thesis
-	    by (rule da_weakenE)
+	  with da_e show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	with valid_e Q valid_A conf_s1 eval_e wt_e
 	obtain "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and "s2\<Colon>\<preceq>(G, L)"
@@ -570,7 +569,7 @@
   qed
 next
   case (AVar A P e1 Q e2 R)
-  have valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" .
+  note valid_e1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }`
   have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
     using AVar.hyps by simp
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} e1.[e2]=\<succ> {R} }"
@@ -674,9 +673,9 @@
   qed
 next
   case (NewA A P T Q e R)
-  have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }" .
-  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; 
-                                            Alloc G (Arr T (the_Intg i)) R}}" .
+  note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }`
+  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; 
+                                            Alloc G (Arr T (the_Intg i)) R}}`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} New T[e]-\<succ> {R} }"
   proof (rule valid_expr_NormalI)
     fix n s0 L accC arrT E v s3 Y Z
@@ -978,7 +977,7 @@
   qed
 next
   case (Acc A P var Q)
-  have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }" .
+  note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} Acc var-\<succ> {Q} }"
   proof (rule valid_expr_NormalI)
     fix n s0 L accC T E v s1 Y Z
@@ -1014,7 +1013,7 @@
   qed
 next
   case (Ass A P var Q e R)
-  have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }" .
+  note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }`
   have valid_e: "\<And> vf. 
                   G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In2 vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R} }"
     using Ass.hyps by simp
@@ -1126,7 +1125,7 @@
   qed
 next
   case (Cond A P e0 P' e1 e2 Q)
-  have valid_e0: "G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }" .
+  note valid_e0 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }`
   have valid_then_else:"\<And> b.  G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q} }"
     using Cond.hyps by simp
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} e0 ? e1 : e2-\<succ> {Q} }"
@@ -1216,7 +1215,7 @@
   qed
 next
   case (Call A P e Q args R mode statT mn pTs' S accC')
-  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }" .
+  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }`
   have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
     using Call.hyps by simp
   have valid_methd: "\<And> a vs invC declC l.
@@ -1605,9 +1604,9 @@
     by (rule Methd_sound)
 next
   case (Body A P D Q c R)
-  have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }".
-  have valid_c: "G,A|\<Turnstile>\<Colon>{ {Q} .c. 
-              {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }".
+  note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }`
+  note valid_c = `G,A|\<Turnstile>\<Colon>{ {Q} .c.
+              {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} Body D c-\<succ> {R} }"
   proof (rule valid_expr_NormalI)
     fix n s0 L accC T E v s4 Y Z
@@ -1780,7 +1779,7 @@
   qed
 next
   case (Expr A P e Q)
-  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }".
+  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Expr e. {Q} }"
   proof (rule valid_stmt_NormalI)
     fix n s0 L accC C s1 Y Z
@@ -1810,7 +1809,7 @@
   qed
 next
   case (Lab A P c l Q)
-  have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }".
+  note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
   proof (rule valid_stmt_NormalI)
     fix n s0 L accC C s2 Y Z
@@ -1847,8 +1846,8 @@
   qed
 next
   case (Comp A P c1 Q c2 R)
-  have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }" .
-  have valid_c2: "G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }" .
+  note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
+  note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1;; c2. {R} }"
   proof (rule valid_stmt_NormalI)
     fix n s0 L accC C s2 Y Z
@@ -1906,8 +1905,8 @@
   qed
 next
   case (If A P e P' c1 c2 Q)
-  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }" .
-  have valid_then_else: "\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} .(if b then c1 else c2). {Q} }" 
+  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }`
+  have valid_then_else: "\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} .(if b then c1 else c2). {Q} }"
     using If.hyps by simp
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .If(e) c1 Else c2. {Q} }"
   proof (rule valid_stmt_NormalI)
@@ -1983,10 +1982,10 @@
   qed
 next
   case (Loop A P e P' c l)
-  have valid_e: "G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }".
-  have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)} 
+  note valid_e = `G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }`
+  note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)}
                          .c. 
-                         {abupd (absorb (Cont l)) .; P} }" .
+                         {abupd (absorb (Cont l)) .; P} }`
   show "G,A|\<Turnstile>\<Colon>{ {P} .l\<bullet> While(e) c. {P'\<leftarrow>=False\<down>=\<diamondsuit>} }"
   proof (rule valid_stmtI)
     fix n s0 L accC C s3 Y Z
@@ -2021,11 +2020,11 @@
 	  (is "PROP ?Hyp n t s v s'")
 	proof (induct)
 	  case (Loop s0' e' n' b s1' c' s2' l' s3' Y' T E)
-	  have while: "(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s" .
+	  note while = `(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
           hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
-	  have valid_A: "\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t". 
-	  have P: "P Y' (Norm s0') Z".
-	  have conf_s0': "Norm s0'\<Colon>\<preceq>(G, L)" .
+	  note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
+	  note P = `P Y' (Norm s0') Z`
+	  note conf_s0' = `Norm s0'\<Colon>\<preceq>(G, L)`
           have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
 	    using Loop.prems eqs by simp
 	  have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
@@ -2123,8 +2122,8 @@
 		    by simp
 		  finally
 		  have "dom (locals (store ((Norm s0')::state))) \<subseteq> \<dots>" .
-		  with da show ?thesis
-		    by (rule da_weakenE)
+		  with da show thesis
+		    by (rule da_weakenE) (rule that)
 		qed
 		from valid_A P_s2' conf_absorb wt da_while'
 		show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z" 
@@ -2240,7 +2239,7 @@
   qed
 next
   case (Throw A P e Q)
-  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }".
+  note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Throw e. {Q} }"
   proof (rule valid_stmt_NormalI)
     fix n s0 L accC C s2 Y Z
@@ -2278,11 +2277,11 @@
   qed
 next
   case (Try A P c1 Q C vn c2 R)
-  have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }".
-  have valid_c2: "G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} 
+  note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }`
+  note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} 
                            .c2. 
-                          {R} }".
-  have Q_R: "(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R" .
+                          {R} }`
+  note Q_R = `(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R`
   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Try c1 Catch(C vn) c2. {R} }"
   proof (rule valid_stmt_NormalI)
     fix n s0 L accC E s3 Y Z
@@ -2409,8 +2408,8 @@
     qed
   qed
 next
-  case (Fin A P c1 Q  c2 R)
-  have valid_c1: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }".
+  case (Fin A P c1 Q c2 R)
+  note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
   have valid_c2: "\<And> abr. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. abr = fst s) ;. abupd (\<lambda>x. None)} 
                                   .c2.
                                   {abupd (abrupt_if (abr \<noteq> None) abr) .; R} }"
@@ -2507,11 +2506,11 @@
   qed
 next
   case (Init C c A P Q R)
-  have c: "the (class G C) = c".
-  have valid_super: 
-        "G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
+  note c = `the (class G C) = c`
+  note valid_super =
+        `G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
                  .(if C = Object then Skip else Init (super c)). 
-                 {Q} }".
+                 {Q} }`
   have valid_init: 
         "\<And> l.  G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty} 
                         .init c.
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -349,10 +349,10 @@
       by (cases binop) (simp_all)
   next
     case (Cond c e1 e2 b)
-    have hyp_c:  "\<And> b. ?Const b c \<Longrightarrow> ?Ass b c" .
-    have hyp_e1: "\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1" .
-    have hyp_e2: "\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2" .
-    have const: "constVal (c ? e1 : e2) = Some (Bool b)" .
+    note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
+    note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
+    note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
+    note const = `constVal (c ? e1 : e2) = Some (Bool b)`
     then obtain bv where bv: "constVal c = Some bv"
       by simp
     hence emptyC: "assignsE c = {}" by (rule assignsE_const_simp)
@@ -397,10 +397,10 @@
       by (cases binop) (simp_all)
   next
     case (Cond c e1 e2 b)
-    have hyp_c:  "\<And> b. ?Const b c \<Longrightarrow> ?Ass b c" .
-    have hyp_e1: "\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1" .
-    have hyp_e2: "\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2" .
-    have const: "constVal (c ? e1 : e2) = Some (Bool b)" .
+    note hyp_c = `\<And> b. ?Const b c \<Longrightarrow> ?Ass b c`
+    note hyp_e1 = `\<And> b. ?Const b e1 \<Longrightarrow> ?Ass b e1`
+    note hyp_e2 = `\<And> b. ?Const b e2 \<Longrightarrow> ?Ass b e2`
+    note const = `constVal (c ? e1 : e2) = Some (Bool b)`
     then obtain bv where bv: "constVal c = Some bv"
       by simp
     show ?case
@@ -958,8 +958,8 @@
     case (Cast T e)
     have "E\<turnstile>e\<Colon>- (PrimT Boolean)"
     proof -
-      have "E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)" .
-      then obtain Te where "E\<turnstile>e\<Colon>-Te"
+      from `E\<turnstile>(Cast T e)\<Colon>- (PrimT Boolean)`
+      obtain Te where "E\<turnstile>e\<Colon>-Te"
                            "prg E\<turnstile>Te\<preceq>? PrimT Boolean"
 	by cases simp
       thus ?thesis
@@ -988,10 +988,10 @@
       by - (cases binop, auto simp add: assignsE_const_simp)
   next
     case (Cond c e1 e2)
-    have hyp_c: "?Boolean c \<Longrightarrow> ?Incl c" .
-    have hyp_e1: "?Boolean e1 \<Longrightarrow> ?Incl e1" .
-    have hyp_e2: "?Boolean e2 \<Longrightarrow> ?Incl e2" .
-    have wt: "E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean" .
+    note hyp_c = `?Boolean c \<Longrightarrow> ?Incl c`
+    note hyp_e1 = `?Boolean e1 \<Longrightarrow> ?Incl e1`
+    note hyp_e2 = `?Boolean e2 \<Longrightarrow> ?Incl e2`
+    note wt = `E\<turnstile>(c ? e1 : e2)\<Colon>-PrimT Boolean`
     then obtain
       boolean_c:  "E\<turnstile>c\<Colon>-PrimT Boolean" and
       boolean_e1: "E\<turnstile>e1\<Colon>-PrimT Boolean" and
@@ -1049,9 +1049,9 @@
   by (auto simp add: range_inter_ts_def)
 
 lemma da_monotone: 
-      assumes      da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A"   and
-        subseteq_B_B': "B \<subseteq> B'"          and
-                  da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" 
+  assumes da: "Env\<turnstile> B  \<guillemotright>t\<guillemotright> A" and
+    "B \<subseteq> B'" and
+    da': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" 
   shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
 proof -
   from da
@@ -1068,10 +1068,10 @@
     show ?case by cases simp
   next
     case (Lab Env B c C A l B' A')
-    have A: "nrm A = nrm C \<inter> brk C l" "brk A = rmlab l (brk C)" .
-    have "PROP ?Hyp Env B \<langle>c\<rangle> C" .
+    note A = `nrm A = nrm C \<inter> brk C l` `brk A = rmlab l (brk C)`
+    note `PROP ?Hyp Env B \<langle>c\<rangle> C`
     moreover
-    have "B \<subseteq> B'" .
+    note `B \<subseteq> B'`
     moreover
     obtain C'
       where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
@@ -1094,40 +1094,40 @@
       by simp
   next
     case (Comp Env B c1 C1 c2 C2 A B' A')
-    have A: "nrm A = nrm C2" "brk A = brk C1 \<Rightarrow>\<inter>  brk C2" .
-    have "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'" .
-    then obtain  C1' C2'
+    note A = `nrm A = nrm C2` `brk A = brk C1 \<Rightarrow>\<inter>  brk C2`
+    from `Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'`
+    obtain  C1' C2'
       where da_c1: "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
             da_c2: "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"  and
             A': "nrm A' = nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"
       by (rule da_elim_cases) auto
-    have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" .
-    moreover have "B \<subseteq> B'" .
+    note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
+    moreover note `B \<subseteq> B'`
     moreover note da_c1
     ultimately have C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
-      by (auto)
-    have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2" .
+      by auto
+    note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle> C2`
     with da_c2 C1' 
     have C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
-      by (auto)
+      by auto
     with A A' C1'
     show ?case
       by auto
   next
     case (If Env B e E c1 C1 c2 C2 A B' A')
-    have A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter>  brk C2" .
-    have "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'" .
-    then obtain C1' C2'
+    note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter>  brk C2`
+    from `Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'`
+    obtain C1' C2'
       where da_c1: "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
             da_c2: "Env\<turnstile> B' \<union> assigns_if False e \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
                A': "nrm A' = nrm C1' \<inter> nrm C2'" "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'"
       by (rule da_elim_cases) auto
-    have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1" .
-    moreover have B': "B \<subseteq> B'" .
+    note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle> C1`
+    moreover note B' = `B \<subseteq> B'`
     moreover note da_c1 
     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
       by blast
-    have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2" .
+    note `PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle> C2`
     with da_c2 B'
     obtain C2': "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
       by blast
@@ -1136,17 +1136,16 @@
       by auto
   next
     case (Loop Env B e E c C A l B' A')
-    have A: "nrm A = nrm C \<inter> (B \<union> assigns_if False e)"
-            "brk A = brk C" .
-    have "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'" .
-    then obtain C'
+    note A = `nrm A = nrm C \<inter> (B \<union> assigns_if False e)` `brk A = brk C`
+    from `Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'`
+    obtain C'
       where 
        da_c': "Env\<turnstile> B' \<union> assigns_if True e \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
           A': "nrm A' = nrm C' \<inter> (B' \<union> assigns_if False e)"
               "brk A' = brk C'" 
       by (rule da_elim_cases) auto
-    have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C" .
-    moreover have B': "B \<subseteq> B'" .
+    note `PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle> C`
+    moreover note B' = `B \<subseteq> B'`
     moreover note da_c'
     ultimately obtain C': "nrm C \<subseteq> nrm C'" "(\<forall>l. brk C l \<subseteq> brk C' l)"
       by blast
@@ -1177,23 +1176,22 @@
     case Throw thus ?case by -  (erule da_elim_cases, auto)
   next
     case (Try Env B c1 C1 vn C c2 C2 A B' A')
-    have A: "nrm A = nrm C1 \<inter> nrm C2"
-            "brk A = brk C1 \<Rightarrow>\<inter>  brk C2" .
-    have "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'" .
-    then obtain C1' C2'
+    note A = `nrm A = nrm C1 \<inter> nrm C2` `brk A = brk C1 \<Rightarrow>\<inter>  brk C2`
+    from `Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'`
+    obtain C1' C2'
       where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
             da_c2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile> B' \<union> {VName vn} 
                       \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
             A': "nrm A' = nrm C1' \<inter> nrm C2'"
                 "brk A' = brk C1' \<Rightarrow>\<inter>  brk C2'" 
       by (rule da_elim_cases) auto
-    have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" .
-    moreover have B': "B \<subseteq> B'" .
+    note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
+    moreover note B' = `B \<subseteq> B'`
     moreover note da_c1'
     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
       by blast
-    have "PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
-                    (B \<union> {VName vn}) \<langle>c2\<rangle> C2" .
+    note `PROP ?Hyp (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>)
+                    (B \<union> {VName vn}) \<langle>c2\<rangle> C2`
     with B' da_c2'
     obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
       by blast
@@ -1202,21 +1200,21 @@
       by auto
   next
     case (Fin Env B c1 C1 c2 C2 A B' A')
-    have A: "nrm A = nrm C1 \<union> nrm C2"
-            "brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)" .
-    have "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'" .
-    then obtain C1' C2'
+    note A = `nrm A = nrm C1 \<union> nrm C2`
+      `brk A = (brk C1 \<Rightarrow>\<union>\<^sub>\<forall> nrm C2) \<Rightarrow>\<inter> (brk C2)`
+    from `Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'`
+    obtain C1' C2'
       where  da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
              da_c2': "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
              A':  "nrm A' = nrm C1' \<union> nrm C2'"
                   "brk A' = (brk C1' \<Rightarrow>\<union>\<^sub>\<forall> nrm C2') \<Rightarrow>\<inter> (brk C2')"
       by (rule da_elim_cases) auto
-    have "PROP ?Hyp Env B \<langle>c1\<rangle> C1" .
-    moreover have B': "B \<subseteq> B'" .
+    note `PROP ?Hyp Env B \<langle>c1\<rangle> C1`
+    moreover note B' = `B \<subseteq> B'`
     moreover note da_c1'
     ultimately obtain C1': "nrm C1 \<subseteq> nrm C1'" "(\<forall>l. brk C1 l \<subseteq> brk C1' l)"
       by blast
-    have hyp_c2: "PROP ?Hyp Env B \<langle>c2\<rangle> C2" .
+    note hyp_c2 = `PROP ?Hyp Env B \<langle>c2\<rangle> C2`
     from da_c2' B' 
      obtain "nrm C2 \<subseteq> nrm C2'" "(\<forall>l. brk C2 l \<subseteq> brk C2' l)"
        by - (drule hyp_c2,auto)
@@ -1239,17 +1237,17 @@
      case UnOp thus ?case by -  (erule da_elim_cases, auto)
    next
      case (CondAnd Env B e1 E1 e2 E2 A B' A')
-     have A: "nrm A = B \<union>
+     note A = `nrm A = B \<union>
                        assigns_if True (BinOp CondAnd e1 e2) \<inter>
-                       assigns_if False (BinOp CondAnd e1 e2)"
-             "brk A = (\<lambda>l. UNIV)" .
-     have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'" .
-     then obtain  A': "nrm A' = B' \<union>
+                       assigns_if False (BinOp CondAnd e1 e2)`
+             `brk A = (\<lambda>l. UNIV)`
+     from `Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'`
+     obtain  A': "nrm A' = B' \<union>
                                  assigns_if True (BinOp CondAnd e1 e2) \<inter>
                                  assigns_if False (BinOp CondAnd e1 e2)"
                       "brk A' = (\<lambda>l. UNIV)" 
        by (rule da_elim_cases) auto
-     have B': "B \<subseteq> B'" .
+     note B' = `B \<subseteq> B'`
      with A A' show ?case 
        by auto 
    next
@@ -1268,13 +1266,13 @@
      case Ass thus ?case by -  (erule da_elim_cases, auto)
    next
      case (CondBool Env c e1 e2 B C E1 E2 A B' A')
-     have A: "nrm A = B \<union> 
+     note A = `nrm A = B \<union> 
                         assigns_if True (c ? e1 : e2) \<inter> 
-                        assigns_if False (c ? e1 : e2)"
-             "brk A = (\<lambda>l. UNIV)" .
-     have "Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)" .
+                        assigns_if False (c ? e1 : e2)`
+             `brk A = (\<lambda>l. UNIV)`
+     note `Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
      moreover
-     have "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" .
+     note `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
      ultimately
      obtain A': "nrm A' = B' \<union> 
                                   assigns_if True (c ? e1 : e2) \<inter> 
@@ -1282,16 +1280,15 @@
                      "brk A' = (\<lambda>l. UNIV)"
        by - (erule da_elim_cases,auto simp add: inj_term_simps) 
        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
-     have B': "B \<subseteq> B'" .
+     note B' = `B \<subseteq> B'`
      with A A' show ?case 
        by auto 
    next
      case (Cond Env c e1 e2 B C E1 E2 A B' A')  
-     have A: "nrm A = nrm E1 \<inter> nrm E2"
-             "brk A = (\<lambda>l. UNIV)" .
-     have not_bool: "\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)" .
-     have "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'" .
-     then obtain E1' E2'
+     note A = `nrm A = nrm E1 \<inter> nrm E2` `brk A = (\<lambda>l. UNIV)`
+     note not_bool = `\<not> Env\<turnstile> (c ? e1 : e2)\<Colon>- (PrimT Boolean)`
+     from `Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'`
+     obtain E1' E2'
        where da_e1': "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
              da_e2': "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
                  A': "nrm A' = nrm E1' \<inter> nrm E2'"
@@ -1299,12 +1296,12 @@
        using not_bool
        by  - (erule da_elim_cases, auto simp add: inj_term_simps)
        (* inj_term_simps needed to handle wt (defined without \<langle>\<rangle>) *)
-     have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1" .
-     moreover have B': "B \<subseteq> B'" .
+     note `PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle> E1`
+     moreover note B' = `B \<subseteq> B'`
      moreover note da_e1'
      ultimately obtain E1': "nrm E1 \<subseteq> nrm E1'" "(\<forall>l. brk E1 l \<subseteq> brk E1' l)"
-      by blast
-     have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2" .
+       by blast
+     note `PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle> E2`
      with B' da_e2'
      obtain "nrm E2 \<subseteq> nrm E2'" "(\<forall>l. brk E2 l \<subseteq> brk E2' l)"
        by blast
@@ -1330,12 +1327,11 @@
   next
     case Cons thus ?case by -  (erule da_elim_cases, auto)
   qed
-qed
+qed (rule da', rule `B \<subseteq> B'`)
   
 lemma da_weaken:     
-      assumes            da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and
-              subseteq_B_B': "B \<subseteq> B'" 
-        shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
+  assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'" 
+  shows "\<exists> A'. Env \<turnstile> B' \<guillemotright>t\<guillemotright> A'"
 proof -
   note assigned.select_convs [Pure.intro]
   from da  
@@ -1346,9 +1342,9 @@
     case Expr thus ?case by (iprover intro: da.Expr)
   next
     case (Lab Env B c C A l B')  
-    have "PROP ?Hyp Env B \<langle>c\<rangle>" .
+    note `PROP ?Hyp Env B \<langle>c\<rangle>`
     moreover
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
       by iprover
     then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
@@ -1356,10 +1352,10 @@
     thus ?case ..
   next
     case (Comp Env B c1 C1 c2 C2 A B')
-    have da_c1: "Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" .
-    have "PROP ?Hyp Env B \<langle>c1\<rangle>" .
+    note da_c1 = `Env\<turnstile> B \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1`
+    note `PROP ?Hyp Env B \<langle>c1\<rangle>`
     moreover
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
       by iprover
     with da_c1 B'
@@ -1367,7 +1363,7 @@
       "nrm C1 \<subseteq> nrm C1'"
       by (rule da_monotone [elim_format]) simp
     moreover
-    have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>" .
+    note `PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>`
     ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
       by iprover
     with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
@@ -1375,7 +1371,7 @@
     thus ?case ..
   next
     case (If Env B e E c1 C1 c2 C2 A B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain  E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
@@ -1409,8 +1405,8 @@
     thus ?case ..
   next  
     case (Loop Env B e E c C A l B')
-    have B': "B \<subseteq> B'" .
-    obtain  E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
+    note B' = `B \<subseteq> B'`
+    obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
       with B'  
@@ -1433,7 +1429,7 @@
     thus ?case ..
   next
     case (Jmp jump B A Env B') 
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     with Jmp.hyps have "jump = Ret \<longrightarrow> Result \<in> B' "
       by auto
     moreover
@@ -1452,7 +1448,7 @@
     case Throw thus ?case by (iprover intro: da.Throw )
   next
     case (Try Env B c1 C1 vn C c2 C2 A B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain C1' where "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
     proof -
       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
@@ -1477,7 +1473,7 @@
     thus ?case ..
   next
     case (Fin Env B c1 C1 c2 C2 A B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain C1' where C1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
     proof -
       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
@@ -1511,11 +1507,11 @@
     case UnOp thus ?case by (iprover intro: da.UnOp)
   next
     case (CondAnd Env B e1 E1 e2 E2 A B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
-      with B'  
+      with B'
       show ?thesis using that by iprover
     qed
     moreover
@@ -1533,7 +1529,7 @@
     thus ?case ..
   next
     case (CondOr Env B e1 E1 e2 E2 A B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain E1' where "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
@@ -1555,11 +1551,11 @@
     thus ?case ..
   next
     case (BinOp Env B e1 E1 e2 A binop B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
-      with B'  
+      with B'
       show ?thesis using that by iprover
     qed
     moreover
@@ -1579,22 +1575,22 @@
     thus ?case ..
   next
     case (Super B Env B')
-    have B': "B \<subseteq> B'" .
-    with Super.hyps have "This \<in> B' "
+    note B' = `B \<subseteq> B'`
+    with Super.hyps have "This \<in> B'"
       by auto
     thus ?case by (iprover intro: da.Super)
   next
     case (AccLVar vn B A Env B')
-    have "vn \<in> B" .
+    note `vn \<in> B`
     moreover
-    have "B \<subseteq> B'" .
+    note `B \<subseteq> B'`
     ultimately have "vn \<in> B'" by auto
     thus ?case by (iprover intro: da.AccLVar)
   next
     case Acc thus ?case by (iprover intro: da.Acc)
   next 
     case (AssLVar Env B e E A vn B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
       by (rule AssLVar.hyps [elim_format]) iprover
     then obtain A' where  
@@ -1603,8 +1599,8 @@
     thus ?case ..
   next
     case (Ass v Env B V e A B') 
-    have B': "B \<subseteq> B'" .
-    have "\<forall>vn. v \<noteq> LVar vn".
+    note B' = `B \<subseteq> B'`
+    note `\<forall>vn. v \<noteq> LVar vn`
     moreover
     obtain V' where V': "Env\<turnstile> B' \<guillemotright>\<langle>v\<rangle>\<guillemotright> V'"
     proof -
@@ -1629,8 +1625,8 @@
     thus ?case ..
   next
     case (CondBool Env c e1 e2 B C E1 E2 A B')
-    have B': "B \<subseteq> B'" .
-    have "Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" .
+    note B' = `B \<subseteq> B'`
+    note `Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
     proof -
       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
@@ -1665,8 +1661,8 @@
     thus ?case ..
   next
     case (Cond Env c e1 e2 B C E1 E2 A B')
-    have B': "B \<subseteq> B'" .
-    have "\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)" .
+    note B' = `B \<subseteq> B'`
+    note `\<not> Env\<turnstile>(c ? e1 : e2)\<Colon>-(PrimT Boolean)`
     moreover obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
     proof -
       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
@@ -1701,7 +1697,7 @@
     thus ?case ..
   next
     case (Call Env B e E args A accC statT mode mn pTs B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
@@ -1727,7 +1723,7 @@
     case Methd thus ?case by (iprover intro: da.Methd)
   next
     case (Body Env B c C A D B')  
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain C' where C': "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and nrm_C': "nrm C \<subseteq> nrm C'"
     proof -
       have "Env\<turnstile> B \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" by (rule Body.hyps)
@@ -1741,10 +1737,10 @@
       with da_c that show ?thesis by iprover
     qed
     moreover 
-    have "Result \<in> nrm C" .
+    note `Result \<in> nrm C`
     with nrm_C' have "Result \<in> nrm C'"
       by blast
-    moreover have "jumpNestingOkS {Ret} c" .
+    moreover note `jumpNestingOkS {Ret} c`
     ultimately obtain A' where
       "Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
       by (iprover intro: da.Body)
@@ -1755,11 +1751,11 @@
     case FVar thus ?case by (iprover intro: da.FVar)
   next
     case (AVar Env B e1 E1 e2 A B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain E1' where E1': "Env\<turnstile> B' \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
-      with B'  
+      with B'
       show ?thesis using that by iprover
     qed
     moreover
@@ -1781,7 +1777,7 @@
     case Nil thus ?case by (iprover intro: da.Nil)
   next
     case (Cons Env B e E es A B')
-    have B': "B \<subseteq> B'" .
+    note B' = `B \<subseteq> B'`
     obtain E' where E': "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
@@ -1804,7 +1800,7 @@
       by (iprover intro: da.Cons)
     thus ?case ..
   qed
-qed
+qed (rule `B \<subseteq> B'`)
 
 (* Remarks about the proof style:
 
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -1,3 +1,5 @@
+(* $Id$ *)
+
 header {* Correctness of Definite Assignment *}
 
 theory DefiniteAssignmentCorrect imports WellForm Eval begin
@@ -107,8 +109,8 @@
        and True
   proof (induct rule: var_expr_stmt.inducts)
     case (Lab j c jmps' jmps)
-    have jmpOk: "jumpNestingOkS jmps' (j\<bullet> c)" .
-    have jmps: "jmps' \<subseteq> jmps" .
+    note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
+    note jmps = `jmps' \<subseteq> jmps`
     with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp
     moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto
     ultimately
@@ -138,10 +140,11 @@
       by simp
   next
     case (Loop l e c jmps' jmps)
-    have "jumpNestingOkS jmps' (l\<bullet> While(e) c)" .
-    hence "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
-    moreover have "jmps' \<subseteq> jmps" .
-    hence "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps" by auto
+    from `jumpNestingOkS jmps' (l\<bullet> While(e) c)`
+    have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
+    moreover
+    from `jmps' \<subseteq> jmps`
+    have "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps" by auto
     ultimately
     have "jumpNestingOkS ({Cont l} \<union> jmps) c"
       by (rule Loop.hyps)
@@ -310,8 +313,8 @@
     case Expr thus ?case by (elim wt_elim_cases) simp
   next
     case (Lab s0 c s1 jmp jmps T Env) 
-    have jmpOK: "jumpNestingOk jmps (In1r (jmp\<bullet> c))" .
-    have G: "prg Env = G" .
+    note jmpOK = `jumpNestingOk jmps (In1r (jmp\<bullet> c))`
+    note G = `prg Env = G`
     have wt_c: "Env\<turnstile>c\<Colon>\<surd>" 
       using Lab.prems by (elim wt_elim_cases)
     { 
@@ -321,7 +324,7 @@
       proof -
         from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
           by (cases s1) (simp add: absorb_def)
-        have hyp_c: "PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>" .
+        note hyp_c = `PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>`
         from ab_s1 have "j \<noteq> jmp" 
           by (cases s1) (simp add: absorb_def)
         moreover have "j \<in> {jmp} \<union> jmps"
@@ -339,9 +342,9 @@
     thus ?case by simp
   next
     case (Comp s0 c1 s1 c2 s2 jmps T Env)
-    have jmpOk: "jumpNestingOk jmps (In1r (c1;; c2))" .
-    have G: "prg Env = G" .
-    from Comp.prems obtain 
+    note jmpOk = `jumpNestingOk jmps (In1r (c1;; c2))`
+    note G = `prg Env = G`
+    from Comp.prems obtain
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
     {
@@ -351,11 +354,11 @@
       proof -
         have jmp: "?Jmp jmps s1"
         proof -
-          have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>" .
+          note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>`
           with wt_c1 jmpOk G 
           show ?thesis by simp
         qed
-        moreover have hyp_c2: "PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)" .
+        moreover note hyp_c2 = `PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)`
         have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
         moreover note wt_c2 G abr_s2
         ultimately show "j \<in> jmps"
@@ -364,8 +367,8 @@
     } thus ?case by simp
   next
     case (If s0 e b s1 c1 c2 s2 jmps T Env)
-    have jmpOk: "jumpNestingOk jmps (In1r (If(e) c1 Else c2))" .
-    have G: "prg Env = G" .
+    note jmpOk = `jumpNestingOk jmps (In1r (If(e) c1 Else c2))`
+    note G = `prg Env = G`
     from If.prems obtain 
               wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
       wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
@@ -375,11 +378,11 @@
       assume jmp: "abrupt s2 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .
+        note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
         with wt_e G have "?Jmp jmps s1" 
           by simp
-        moreover have hyp_then_else: 
-          "PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>" .
+        moreover note hyp_then_else =
+          `PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>`
         have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
           using jmpOk by (cases "the_Bool b") simp_all
         moreover note wt_then_else G jmp
@@ -390,9 +393,9 @@
     thus ?case by simp
   next
     case (Loop s0 e b s1 c s2 l s3 jmps T Env)
-    have jmpOk: "jumpNestingOk jmps (In1r (l\<bullet> While(e) c))" .
-    have G: "prg Env = G" .
-    have wt: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
+    note jmpOk = `jumpNestingOk jmps (In1r (l\<bullet> While(e) c))`
+    note G = `prg Env = G`
+    note wt = `Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
     then obtain 
               wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
               wt_c: "Env\<turnstile>c\<Colon>\<surd>"
@@ -402,7 +405,7 @@
       assume jmp: "abrupt s3 = Some (Jump j)" 
       have "j\<in>jmps"
       proof -
-        have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)" .
+        note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
         with wt_e G have jmp_s1: "?Jmp jmps s1" 
           by simp
         show ?thesis
@@ -470,8 +473,8 @@
     case (Jmp s j jmps T Env) thus ?case by simp
   next
     case (Throw s0 e a s1 jmps T Env)
-    have jmpOk: "jumpNestingOk jmps (In1r (Throw e))" .
-    have G: "prg Env = G" .
+    note jmpOk = `jumpNestingOk jmps (In1r (Throw e))`
+    note G = `prg Env = G`
     from Throw.prems obtain Te where 
       wt_e: "Env\<turnstile>e\<Colon>-Te" 
       by (elim wt_elim_cases)
@@ -480,8 +483,8 @@
       assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .
-        hence "?Jmp jmps s1" using wt_e G by simp
+        from `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
+        have "?Jmp jmps s1" using wt_e G by simp
         moreover
         from jmp 
         have "abrupt s1 = Some (Jump j)"
@@ -492,8 +495,8 @@
     thus ?case by simp
   next
     case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
-    have jmpOk: "jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))" .
-    have G: "prg Env = G" .
+    note jmpOk = `jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))`
+    note G = `prg Env = G`
     from Try.prems obtain 
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and  
       wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
@@ -503,10 +506,10 @@
       assume jmp: "abrupt s3 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have "PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)" .
+        note `PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)`
         with jmpOk wt_c1 G
         have jmp_s1: "?Jmp jmps s1" by simp
-        have s2: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
+        note s2 = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
         show "j \<in> jmps"
         proof (cases "G,s2\<turnstile>catch C")
           case False
@@ -544,8 +547,8 @@
     thus ?case by simp
   next
     case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
-    have jmpOk: " jumpNestingOk jmps (In1r (c1 Finally c2))" .
-    have G: "prg Env = G" .
+    note jmpOk = `jumpNestingOk jmps (In1r (c1 Finally c2))`
+    note G = `prg Env = G`
     from Fin.prems obtain 
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
@@ -555,16 +558,16 @@
       have "j \<in> jmps"
       proof (cases "x1=Some (Jump j)")
         case True
-        have hyp_c1: "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>" .
+        note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>`
         with True jmpOk wt_c1 G show ?thesis 
           by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
       next
         case False
-        have hyp_c2:  "PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>" .
-        have "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
-                             else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+        note hyp_c2 = `PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>`
+        note `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
         with False jmp have "abrupt s2 = Some (Jump j)"
-          by (cases s2, simp add: abrupt_if_def)
+          by (cases s2) (simp add: abrupt_if_def)
         with jmpOk wt_c2 G show ?thesis 
           by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)
       qed
@@ -572,9 +575,9 @@
     thus ?case by simp
   next
     case (Init C c s0 s3 s1 s2 jmps T Env)
-    have "jumpNestingOk jmps (In1r (Init C))".
-    have G: "prg Env = G" .
-    have "the (class G C) = c" .
+    note `jumpNestingOk jmps (In1r (Init C))`
+    note G = `prg Env = G`
+    note `the (class G C) = c`
     with Init.prems have c: "class G C = Some c"
       by (elim wt_elim_cases) auto
     {
@@ -642,16 +645,15 @@
       assume jmp: "abrupt s2 = Some (Jump j)"
       have "j\<in>jmps"
       proof - 
-        have "prg Env = G" .
-        moreover have hyp_init: "PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>" .
+        note `prg Env = G`
+        moreover note hyp_init = `PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>`
         moreover from wf NewC.prems 
         have "Env\<turnstile>(Init C)\<Colon>\<surd>"
           by (elim wt_elim_cases) (drule is_acc_classD,simp)
         moreover 
         have "abrupt s1 = Some (Jump j)"
         proof -
-          have "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
-          from this jmp show ?thesis
+          from `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2` and jmp show ?thesis
             by (rule halloc_no_jump')
         qed
         ultimately show "j \<in> jmps" 
@@ -666,20 +668,20 @@
       assume jmp: "abrupt s3 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have G: "prg Env = G" .
+	note G = `prg Env = G`
         from NewA.prems 
         obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
                wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
           by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
-        have "PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>" .
+        note `PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>`
         with wt_init G 
         have "?Jmp jmps s1" 
           by (simp add: init_comp_ty_def)
         moreover
-        have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 i)" .
+        note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 i)`
         have "abrupt s2 = Some (Jump j)"
         proof -
-          have "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
+          note `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
           moreover note jmp
           ultimately 
           have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
@@ -698,14 +700,14 @@
       assume jmp: "abrupt s2 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
-        have "prg Env = G" .
+        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+        note `prg Env = G`
         moreover from Cast.prems
         obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
         moreover 
         have "abrupt s1 = Some (Jump j)"
         proof -
-          have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .
+          note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
           moreover note jmp
           ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
         qed
@@ -721,8 +723,8 @@
       assume jmp: "abrupt s1 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
-        have "prg Env = G" .
+        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+        note `prg Env = G`
         moreover from Inst.prems
         obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
         moreover note jmp
@@ -740,8 +742,8 @@
       assume jmp: "abrupt s1 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
-        have "prg Env = G" .
+        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
+        note `prg Env = G`
         moreover from UnOp.prems
         obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
         moreover note jmp
@@ -757,17 +759,17 @@
       assume jmp: "abrupt s2 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have G: "prg Env = G" .
+        note G = `prg Env = G`
         from BinOp.prems
         obtain e1T e2T where 
           wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
           wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
           by (elim wt_elim_cases)
-        have "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)" .
+        note `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)`
         with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
-        have hyp_e2: 
-          "PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
-                     s1 s2 (In1 v2)" .
+        note hyp_e2 =
+          `PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
+                     s1 s2 (In1 v2)`
         show "j\<in>jmps"
         proof (cases "need_second_arg binop v1")
           case True with jmp_s1 wt_e2 jmp G
@@ -790,8 +792,8 @@
       assume jmp: "abrupt s1 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_va: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))" .
-        have "prg Env = G" .
+        note hyp_va = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))`
+        note `prg Env = G`
         moreover from Acc.prems
         obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
         moreover note jmp
@@ -802,14 +804,14 @@
     thus ?case by simp
   next
     case (Ass s0 va w f s1 e v s2 jmps T Env)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Ass.prems
     obtain vT eT where
       wt_va: "Env\<turnstile>va\<Colon>=vT" and
        wt_e: "Env\<turnstile>e\<Colon>-eT"
       by (elim wt_elim_cases)
-    have hyp_v: "PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))" .
-    have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 v)" . 
+    note hyp_v = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))`
+    note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 v)`
     {
       fix j
       assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
@@ -818,8 +820,7 @@
         have "abrupt s2 = Some (Jump j)"
         proof (cases "normal s2")
           case True
-          have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
-          from this True have nrm_s1: "normal s1" 
+          from `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2` and True have nrm_s1: "normal s1" 
             by (rule eval_no_abrupt_lemma [rule_format]) 
           with nrm_s1 wt_va G True
           have "abrupt (f v s2) \<noteq> Some (Jump j)"
@@ -836,16 +837,15 @@
         have "?Jmp jmps s1"
           by - (rule hyp_v [THEN conjunct1],simp_all)
         ultimately show ?thesis using G 
-          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)
+          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)
       qed
     }
     thus ?case by simp
   next
     case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)
-    have G: "prg Env = G" .
-    have hyp_e0: "PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)" .
-    have hyp_e1_e2: "PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) 
-                               s1 s2 (In1 v)" .
+    note G = `prg Env = G`
+    note hyp_e0 = `PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)`
+    note hyp_e1_e2 = `PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)`
     from Cond.prems
     obtain e1T e2T
       where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"
@@ -878,7 +878,7 @@
   next
     case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
                jmps T Env)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Call.prems
     obtain eT argsT 
       where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
@@ -889,26 +889,26 @@
                      = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)" .
+        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
         from wt_e G 
         have jmp_s1: "?Jmp jmps s1"
           by - (rule hyp_e [THEN conjunct1],simp_all)
-        have hyp_args: "PROP ?Hyp (In3 args) s1 s2 (In3 vs)" .
+        note hyp_args = `PROP ?Hyp (In3 args) s1 s2 (In3 vs)`
         have "abrupt s2 = Some (Jump j)"
         proof -
-          have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4" .
+          note `G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4`
           moreover
           from jmp have "abrupt s4 = Some (Jump j)"
             by (cases s4) simp
           ultimately have "abrupt s3' = Some (Jump j)"
             by - (rule ccontr,drule (1) Methd_no_jump,simp)
-          moreover have "s3' = check_method_access G accC statT mode 
-                              \<lparr>name = mn, parTs = pTs\<rparr> a s3" .
+          moreover note `s3' = check_method_access G accC statT mode 
+                              \<lparr>name = mn, parTs = pTs\<rparr> a s3`
           ultimately have "abrupt s3 = Some (Jump j)"
             by (cases s3) 
                (simp add: check_method_access_def abrupt_if_def Let_def)
           moreover 
-          have "s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2" .
+          note `s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2`
           ultimately show ?thesis
             by (cases s2) (auto simp add: init_lvars_def2)
         qed
@@ -920,6 +920,7 @@
     thus ?case by simp
   next
     case (Methd s0 D sig v s1 jmps T Env)
+    from `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
     have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
       by (rule eval.Methd)
     hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
@@ -929,7 +930,7 @@
     case (Body s0 D s1 c s2 s3 jmps T Env)
     have "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
            \<rightarrow> abupd (absorb Ret) s3"
-      by (rule eval.Body)
+      by (rule eval.Body) (rule Body)+
     hence "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
       by (rule Body_no_jump) simp
     thus ?case by simp
@@ -938,7 +939,7 @@
     thus ?case by (simp add: lvar_def Let_def)
   next
     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from wf FVar.prems 
     obtain  statC f where
       wt_e: "Env\<turnstile>e\<Colon>-Class statC" and
@@ -955,21 +956,21 @@
       thus ?thesis
         by simp
     qed
-    have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
+    note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
     {
       fix j
       assume jmp: "abrupt s3 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_init: "PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>" .
+        note hyp_init = `PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>`
         from G wt_init 
         have "?Jmp jmps s1"
           by - (rule hyp_init [THEN conjunct1],auto)
         moreover
-        have hyp_e: "PROP ?Hyp (In1l e) s1 s2 (In1 a)" .
+        note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 a)`
         have "abrupt s2 = Some (Jump j)"
         proof -
-          have "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+          note `s3 = check_field_access G accC statDeclC fn stat a s2'`
           with jmp have "abrupt s2' = Some (Jump j)"
             by (cases s2') 
                (simp add: check_field_access_def abrupt_if_def Let_def)
@@ -997,23 +998,23 @@
     ultimately show ?case using v by simp
   next
     case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from AVar.prems 
     obtain  e1T e2T where
       wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
       by  (elim wt_elim_cases) simp
-    have avar: "(v, s2') = avar G i a s2" .
+    note avar = `(v, s2') = avar G i a s2`
     {
       fix j
       assume jmp: "abrupt s2' = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_e1: "PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)" .
+        note hyp_e1 = `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)`
         from G wt_e1
         have "?Jmp jmps s1"
-          by - (rule hyp_e1 [THEN conjunct1],auto)
+          by - (rule hyp_e1 [THEN conjunct1], auto)
         moreover
-        have hyp_e2: "PROP ?Hyp (In1l e2) s1 s2 (In1 i)" .
+        note hyp_e2 = `PROP ?Hyp (In1l e2) s1 s2 (In1 i)`
         have "abrupt s2 = Some (Jump j)"
         proof -
           from avar have "s2' = snd (avar G i a s2)"
@@ -1043,7 +1044,7 @@
     case Nil thus ?case by simp
   next
     case (Cons s0 e v s1 es vs s2 jmps T Env)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Cons.prems obtain eT esT
       where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_e2: "Env\<turnstile>es\<Colon>\<doteq>esT"
       by  (elim wt_elim_cases) simp
@@ -1052,12 +1053,12 @@
       assume jmp: "abrupt s2 = Some (Jump j)"
       have "j\<in>jmps"
       proof -
-        have hyp_e: "PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)" .
+        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
         from G wt_e
         have "?Jmp jmps s1"
           by - (rule hyp_e [THEN conjunct1],simp_all)
         moreover
-        have hyp_es: "PROP ?Hyp (In3 es) s1 s2 (In3 vs)" .  
+        note hyp_es = `PROP ?Hyp (In3 es) s1 s2 (In3 vs)`
         ultimately show ?thesis
           using wt_e2 G jmp
           by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
@@ -1199,7 +1200,7 @@
     by auto
   moreover
   obtain x1 s1 where "f n s = (x1,s1)"
-    by (cases "f n s", simp)
+    by (cases "f n s")
   ultimately
   show ?thesis
     using f_ok
@@ -1338,8 +1339,8 @@
     then
     have s0_s1: "dom (locals (store ((Norm s0)::state))) 
                   \<subseteq> dom (locals (store s1))" by simp
-    have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
-    hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" 
+    from `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
+    have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" 
       by (rule dom_locals_sxalloc_mono)
     thus ?case 
     proof (cases "G,s2\<turnstile>catch C")
@@ -1406,7 +1407,7 @@
     qed
   next
     case (NewC s0 C s1 a s2)
-    have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
+    note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
     from NewC.hyps
     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
       by simp
@@ -1416,7 +1417,7 @@
     finally show ?case by simp
   next
     case (NewA s0 T s1 e i s2 a s3)
-    have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+    note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
     from NewA.hyps
     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
       by simp
@@ -1474,8 +1475,7 @@
       finally show ?thesis by simp
     next
       case False
-      have "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
-      with False 
+      with `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
       have "s2=s1"
 	by auto
       with s0_s1 False
@@ -1497,7 +1497,7 @@
     finally show ?case by simp
   next
     case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
-    have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .
+    note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
     from Call.hyps 
     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
       by simp
@@ -1526,11 +1526,11 @@
     also
     have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
     proof -
-       have "s3 =
+      from `s3 =
          (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
                  abrupt s2 = Some (Jump (Cont l))
-             then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)".
-      thus ?thesis
+             then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
+      show ?thesis
 	by simp
     qed
     finally show ?case by simp
@@ -1551,7 +1551,7 @@
       by (simp add: dom_locals_fvar_vvar_mono) 
     hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s3 \<longrightarrow> ?V_ok)"
       by - (intro strip, simp)
-    have s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+    note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
     from FVar.hyps 
     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
       by simp
@@ -1690,7 +1690,7 @@
     case NewC show ?case by simp
   next
     case (NewA s0 T s1 e i s2 a s3)
-    have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+    note halloc = `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
     proof -
       from NewA
@@ -1733,8 +1733,8 @@
     also
     have "\<dots>  \<subseteq> dom (locals (store s2))"
     proof -
-      have "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
-                      else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
+      note `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+                      else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
       thus ?thesis
 	by (rule dom_locals_eval_mono_elim)
     qed
@@ -1757,7 +1757,7 @@
     case Acc thus ?case by simp
   next 
     case (Ass s0 va w f s1 e v s2)
-    have  nrm_ass_s2: "normal (assign f v s2)" .
+    note nrm_ass_s2 = `normal (assign f v s2)`
     hence nrm_s2: "normal s2"
       by (cases s2, simp add: assign_def Let_def)
     with Ass.hyps 
@@ -1848,16 +1848,16 @@
     case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
     have nrm_s2: "normal s2"
     proof -
-      have "normal ((set_lvars (locals (snd s2))) s4)" .
-      hence normal_s4: "normal s4" by simp
+      from `normal ((set_lvars (locals (snd s2))) s4)`
+      have normal_s4: "normal s4" by simp
       hence "normal s3'" using Call.hyps
 	by - (erule eval_no_abrupt_lemma [rule_format]) 
-      moreover have  
-       "s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3".
+      moreover note
+       `s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3`
       ultimately have "normal s3"
 	by (cases s3) (simp add: check_method_access_def Let_def) 
       moreover
-      have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .
+      note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2`
       ultimately show "normal s2"
 	by (cases s2) (simp add: init_lvars_def2)
     qed
@@ -1888,11 +1888,11 @@
     case LVar thus ?case by simp
   next
     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
-    have s3:  "s3 = check_field_access G accC statDeclC fn stat a s2'" .
-    have avar: "(v, s2') = fvar statDeclC stat fn a s2" .
+    note s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
+    note avar = `(v, s2') = fvar statDeclC stat fn a s2`
     have nrm_s2: "normal s2"
     proof -
-      have "normal s3" .
+      note `normal s3`
       with s3 have "normal s2'"
 	by (cases s2') (simp add: check_field_access_def Let_def)
       with avar show "normal s2"
@@ -1917,11 +1917,10 @@
       by simp
   next
     case (AVar s0 e1 a s1 e2 i s2 v s2')
-    have avar: "(v, s2') = avar G i a s2" .
+    note avar = `(v, s2') = avar G i a s2`
     have nrm_s2: "normal s2"
     proof -
-      have "normal s2'" .
-      with avar
+      from avar and `normal s2'`
       show ?thesis by (cases s2) (simp add: avar_def2)
     qed
     with AVar.hyps 
@@ -2024,19 +2023,19 @@
     case Inst hence False by simp thus ?case ..
   next
     case (Lit val c v s0 s)
-    have "constVal (Lit val) = Some c" .
+    note `constVal (Lit val) = Some c`
     moreover
-    have "G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s" .
-    then obtain "v=val" and "normal s"
+    from `G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s`
+    obtain "v=val" and "normal s"
       by cases simp
     ultimately show "v=c \<and> normal s" by simp
   next
     case (UnOp unop e c v s0 s)
-    have const: "constVal (UnOp unop e) = Some c" .
+    note const = `constVal (UnOp unop e) = Some c`
     then obtain ce where ce: "constVal e = Some ce" by simp
-    have "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s" .
-    then obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
-                          v: "v = eval_unop unop ve" 
+    from `G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s`
+    obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
+                     v: "v = eval_unop unop ve"
       by cases simp
     from ce ve
     obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
@@ -2048,13 +2047,13 @@
     show ?case ..
   next
     case (BinOp binop e1 e2 c v s0 s)
-    have const: "constVal (BinOp binop e1 e2) = Some c" .
+    note const = `constVal (BinOp binop e1 e2) = Some c`
     then obtain c1 c2 where c1: "constVal e1 = Some c1" and
                             c2: "constVal e2 = Some c2" and
                              c: "c = eval_binop binop c1 c2"
       by simp
-    have "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s" .
-    then obtain v1 s1 v2
+    from `G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s`
+    obtain v1 s1 v2
       where v1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
             v2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
                                else In1r Skip)\<succ>\<rightarrow> (In1 v2, s)" and
@@ -2095,14 +2094,14 @@
     case Ass hence False by simp thus ?case ..
   next
     case (Cond b e1 e2 c v s0 s)
-    have c: "constVal (b ? e1 : e2) = Some c" .
+    note c = `constVal (b ? e1 : e2) = Some c`
     then obtain cb c1 c2 where
       cb: "constVal b  = Some cb" and
       c1: "constVal e1 = Some c1" and
       c2: "constVal e2 = Some c2"
       by (auto split: bool.splits)
-    have "G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s" .
-    then obtain vb s1
+    from `G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s`
+    obtain vb s1
       where     vb: "G\<turnstile>Norm s0 \<midarrow>b-\<succ>vb\<rightarrow> s1" and
             eval_v: "G\<turnstile>s1 \<midarrow>(if the_Bool vb then e1 else e2)-\<succ>v\<rightarrow> s"
       by cases simp 
@@ -2172,25 +2171,28 @@
     case Inst hence False by simp thus ?case ..
   next
     case (Lit v c)
-    have "constVal (Lit v) = Some c" .
-    hence "c=v" by simp
-    moreover have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
-    hence "typeof empty_dt v = Some (PrimT Boolean)"
+    from `constVal (Lit v) = Some c`
+    have "c=v" by simp
+    moreover
+    from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+    have "typeof empty_dt v = Some (PrimT Boolean)"
       by cases simp
     ultimately show ?case by simp
   next
     case (UnOp unop e c)
-    have "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
-    hence "Boolean = unop_type unop" by cases simp
-    moreover have "constVal (UnOp unop e) = Some c" .
-    then obtain ce where "c = eval_unop unop ce" by auto
+    from `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
+    have "Boolean = unop_type unop" by cases simp
+    moreover
+    from `constVal (UnOp unop e) = Some c`
+    obtain ce where "c = eval_unop unop ce" by auto
     ultimately show ?case by (simp add: eval_unop_type)
   next
     case (BinOp binop e1 e2 c)
-    have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
-    hence "Boolean = binop_type binop" by cases simp
-    moreover have "constVal (BinOp binop e1 e2) = Some c" .
-    then obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
+    from `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
+    have "Boolean = binop_type binop" by cases simp
+    moreover
+    from `constVal (BinOp binop e1 e2) = Some c`
+    obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
     ultimately show ?case by (simp add: eval_binop_type)
   next
     case Super hence False by simp thus ?case ..
@@ -2200,13 +2202,13 @@
     case Ass hence False by simp thus ?case ..
   next
     case (Cond b e1 e2 c)
-    have c: "constVal (b ? e1 : e2) = Some c" .
+    note c = `constVal (b ? e1 : e2) = Some c`
     then obtain cb c1 c2 where
       cb: "constVal b  = Some cb" and
       c1: "constVal e1 = Some c1" and
       c2: "constVal e2 = Some c2"
       by (auto split: bool.splits)
-    have wt: "Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean" .
+    note wt = `Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean`
     then
     obtain T1 T2
       where "Env\<turnstile>b\<Colon>-PrimT Boolean" and
@@ -2255,28 +2257,28 @@
      case Abrupt thus ?case by simp
    next
      case (NewC s0 C s1 a s2)
-     have "Env\<turnstile>NewC C\<Colon>-PrimT Boolean" .
-     hence False 
+     from `Env\<turnstile>NewC C\<Colon>-PrimT Boolean`
+     have False 
        by cases simp
      thus ?case ..
    next
      case (NewA s0 T s1 e i s2 a s3)
-     have "Env\<turnstile>New T[e]\<Colon>-PrimT Boolean" .
-     hence False 
+     from `Env\<turnstile>New T[e]\<Colon>-PrimT Boolean`
+     have False 
        by cases simp
      thus ?case ..
    next
      case (Cast s0 e b s1 s2 T)
-     have s2: "s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1".
+     note s2 = `s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1`
      have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))" 
      proof -
-       have "normal s2" .
-       with s2 have "normal s1"
+       from s2 and `normal s2`
+       have "normal s1"
 	 by (cases s1) simp
        moreover
-       have "Env\<turnstile>Cast T e\<Colon>-PrimT Boolean" .
-       hence "Env\<turnstile>e\<Colon>- PrimT Boolean" 
-	 by (cases) (auto dest: cast_Boolean2)
+       from `Env\<turnstile>Cast T e\<Colon>-PrimT Boolean`
+       have "Env\<turnstile>e\<Colon>- PrimT Boolean" 
+	 by cases (auto dest: cast_Boolean2)
        ultimately show ?thesis 
 	 by (rule Cast.hyps [elim_format]) auto
      qed
@@ -2286,15 +2288,15 @@
      finally show ?case by simp
    next
      case (Inst s0 e v s1 b T)
-     have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and "normal s1" .
-     hence "assignsE e \<subseteq> dom (locals (store s1))"
+     from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1` and `normal s1`
+     have "assignsE e \<subseteq> dom (locals (store s1))"
        by (rule assignsE_good_approx)
      thus ?case
        by simp
    next
      case (Lit s v)
-     have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
-     hence "typeof empty_dt v = Some (PrimT Boolean)"
+     from `Env\<turnstile>Lit v\<Colon>-PrimT Boolean`
+     have "typeof empty_dt v = Some (PrimT Boolean)"
        by cases simp
      then obtain b where "v=Bool b"
        by (cases v) (simp_all add: empty_dt_def)
@@ -2302,13 +2304,13 @@
        by simp
    next
      case (UnOp s0 e v s1 unop)
-     have bool: "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
+     note bool = `Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean`
      hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" 
        by cases (cases unop,simp_all)
      show ?case
      proof (cases "constVal (UnOp unop e)")
        case None
-       have "normal s1" .
+       note `normal s1`
        moreover note bool_e
        ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
 	 by (rule UnOp.hyps [elim_format]) auto
@@ -2324,8 +2326,8 @@
      next
        case (Some c)
        moreover
-       have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
-       hence "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1" 
+       from `prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+       have "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1" 
 	 by (rule eval.UnOp)
        with Some
        have "eval_unop unop v=c"
@@ -2342,7 +2344,7 @@
      qed
    next
      case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
-     have bool: "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
+     note bool = `Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean`
      show ?case
      proof (cases "constVal (BinOp binop e1 e2)") 
        case (Some c)
@@ -2395,8 +2397,8 @@
 	     with condAnd 
 	     have need_second: "need_second_arg binop v1"
 	       by (simp add: need_second_arg_def)
-	     have "normal s2" . 
-	     hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+	     from `normal s2`
+	     have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
 	       by (rule BinOp.hyps [elim_format]) 
                   (simp add: need_second bool_e2)+
 	     with e1_s2
@@ -2415,8 +2417,8 @@
 	       obtain "the_Bool v1=True" and "the_Bool v2 = False"
 		 by (simp add: need_second_arg_def)
 	       moreover
-	       have "normal s2" . 
-	       hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+	       from `normal s2`
+	       have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
 		 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
 	       with e1_s2
 	       have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
@@ -2443,8 +2445,8 @@
 	     with condOr 
 	     have need_second: "need_second_arg binop v1"
 	       by (simp add: need_second_arg_def)
-	     have "normal s2" . 
-	     hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+	     from `normal s2`
+	     have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
 	       by (rule BinOp.hyps [elim_format]) 
                   (simp add: need_second bool_e2)+
 	     with e1_s2
@@ -2463,8 +2465,8 @@
 	       obtain "the_Bool v1=False" and "the_Bool v2 = True"
 		 by (simp add: need_second_arg_def)
 	       moreover
-	       have "normal s2" . 
-	       hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
+	       from `normal s2`
+	       have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
 		 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
 	       with e1_s2
 	       have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
@@ -2486,12 +2488,12 @@
 	 qed  
        next
 	 case False
-	 have "\<not> (binop = CondAnd \<or> binop = CondOr)" .
+	 note `\<not> (binop = CondAnd \<or> binop = CondOr)`
 	 from BinOp.hyps
 	 have
-	  "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
+	   "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
 	   by - (rule eval.BinOp)  
-	 moreover have "normal s2" .
+	 moreover note `normal s2`
 	 ultimately
 	 have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
 	   by (rule assignsE_good_approx)
@@ -2502,38 +2504,37 @@
      qed
    next     
      case Super 
-     have "Env\<turnstile>Super\<Colon>-PrimT Boolean" .
+     note `Env\<turnstile>Super\<Colon>-PrimT Boolean`
      hence False 
        by cases simp
      thus ?case ..
    next
      case (Acc s0 va v f s1)
-     have "prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1"  and "normal s1".
-     hence "assignsV va \<subseteq> dom (locals (store s1))"
+     from `prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1` and `normal s1`
+     have "assignsV va \<subseteq> dom (locals (store s1))"
        by (rule assignsV_good_approx)
      thus ?case by simp
    next
      case (Ass s0 va w f s1 e v s2)
      hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"
        by - (rule eval.Ass)
-     moreover have "normal (assign f v s2)" .
+     moreover note `normal (assign f v s2)`
      ultimately 
      have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"
        by (rule assignsE_good_approx)
      thus ?case by simp
    next
      case (Cond s0 e0 b s1 e1 e2 v s2)
-     have "Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean" .
-     then obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
-                 wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
+     from `Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean`
+     obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
+            wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
        by cases (auto dest: widen_Boolean2)
-     have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
+     note eval_e0 = `prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
      have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
      proof -
        note eval_e0 
        moreover
-       have "normal s2" .
-       with Cond.hyps have "normal s1"
+       from Cond.hyps and `normal s2` have "normal s1"
 	 by - (erule eval_no_abrupt_lemma [rule_format],simp)
        ultimately
        have "assignsE e0 \<subseteq> dom (locals (store s1))"
@@ -2551,15 +2552,15 @@
 	      \<subseteq> dom (locals (store s2))"
        proof (cases "the_Bool b")
 	 case True
-	 have "normal s2" .
-	 hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
+	 from `normal s2`
+	 have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
 	   by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)
 	 thus ?thesis
 	   by blast
        next
 	 case False
-	 have "normal s2" .
-	 hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
+	 from `normal s2`
+	 have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
 	   by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)
 	 thus ?thesis
 	   by blast
@@ -2578,9 +2579,9 @@
        show ?thesis
        proof (cases "the_Bool c")
 	 case True
-	 have "normal s2" .
-	 hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
-	   by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True)
+	 from `normal s2`
+	 have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
+	   by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)
 	 with e0_s2
 	 have "assignsE e0 \<union> assigns_if (the_Bool v) e1  \<subseteq> \<dots>"
 	   by (rule Un_least)
@@ -2588,9 +2589,9 @@
 	   by simp
        next
 	 case False
-	 have "normal s2" .
-	 hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
-	   by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False)
+	 from `normal s2`
+	 have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
+	   by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)
 	 with e0_s2
 	 have "assignsE e0 \<union> assigns_if (the_Bool v) e2  \<subseteq> \<dots>"
 	   by (rule Un_least)
@@ -2606,6 +2607,7 @@
        by - (rule eval.Call)
      hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args)) 
               \<subseteq>  dom (locals (store ((set_lvars (locals (store s2))) s4)))"
+       using `normal ((set_lvars (locals (snd s2))) s4)`
        by (rule assignsE_good_approx)
      thus ?case by simp
    next
@@ -2695,7 +2697,7 @@
          (rule Expr.hyps, auto)
   next 
     case (Lab s0 c s1 j Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Lab.prems
     obtain C l where
       da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
@@ -2754,7 +2756,7 @@
     ultimately show ?case by (intro conjI)
   next
     case (Comp s0 c1 s1 c2 s2 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Comp.prems
     obtain C1 C2
       where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and 
@@ -2765,7 +2767,7 @@
     obtain wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
            wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases) simp
-    have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
+    note `PROP ?Hyp (In1r c1) (Norm s0) s1`
     with wt_c1 da_c1 G 
     obtain nrm_c1: "?NormalAssigned s1 C1" and 
            brk_c1: "?BreakAssigned (Norm s0) s1 C1" and
@@ -2780,7 +2782,7 @@
                nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
                brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
         by (rule da_weakenE) iprover
-      have "PROP ?Hyp (In1r c2) s1 s2" .
+      note `PROP ?Hyp (In1r c2) s1 s2`
       with wt_c2 da_c2' G
       obtain nrm_c2': "?NormalAssigned s2 C2'" and 
              brk_c2': "?BreakAssigned s1 s2 C2'" and
@@ -2800,8 +2802,8 @@
       ultimately show ?thesis by (intro conjI)
     next
       case False
-      have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
-      with False have eq_s1_s2: "s2=s1" by auto
+      with `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
+      have eq_s1_s2: "s2=s1" by auto
       with False have "?NormalAssigned s2 A" by blast
       moreover
       have "?BreakAssigned (Norm s0) s2 A"
@@ -2827,16 +2829,16 @@
     qed
   next
     case (If s0 e b s1 c1 c2 s2 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
     from If.prems
     obtain E C1 C2 where
       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
-     da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
+      da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
                    \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
-     da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
+      da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
                    \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
-     A: "nrm A = nrm C1 \<inter> nrm C2"  "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
+      A: "nrm A = nrm C1 \<inter> nrm C2"  "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
       by (elim da_elim_cases) 
     from If.prems
     obtain 
@@ -2923,15 +2925,15 @@
       moreover
       have "s2 = s1"
       proof -
-	have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
-        with abr show ?thesis  
+	from abr and `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
+        show ?thesis  
 	  by (cases s1) simp
       qed
       ultimately show ?thesis by simp
     qed
   next
     case (Loop s0 e b s1 c s2 l s3 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" 
       by (simp (no_asm_simp))
     from Loop.prems
@@ -3137,7 +3139,7 @@
     ultimately show ?case by (intro conjI)
   next
     case (Throw s0 e a s1 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Throw.prems obtain E where 
       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"
       by (elim da_elim_cases)
@@ -3167,7 +3169,7 @@
     ultimately show ?case by (intro conjI)
   next
     case (Try s0 c1 s1 s2 C vn c2 s3 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Try.prems obtain C1 C2 where
       da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1"  and
       da_c2:
@@ -3181,7 +3183,7 @@
       by (elim wt_elim_cases)
     have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G 
       by (simp (no_asm_simp))
-    have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
+    note `PROP ?Hyp (In1r c1) (Norm s0) s1`
     with wt_c1 da_c1 G
     obtain nrm_C1: "?NormalAssigned s1 C1" and
            brk_C1: "?BreakAssigned (Norm s0) s1 C1" and
@@ -3239,8 +3241,8 @@
           have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
                   \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
           proof -
-            have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
-            hence "dom (locals (store ((Norm s0)::state))) 
+            from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+            have "dom (locals (store ((Norm s0)::state))) 
                     \<subseteq> dom (locals (store s1))"
               by (rule dom_locals_eval_mono_elim)
             also
@@ -3314,7 +3316,7 @@
     qed
   next
     case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Fin.prems obtain C1 C2 where 
       da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
       da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
@@ -3325,7 +3327,7 @@
       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
       wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
       by (elim wt_elim_cases)
-    have "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)" .
+    note `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)`
     with wt_c1 da_C1 G
     obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and
            brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and
@@ -3345,7 +3347,7 @@
         nrm_C2': "nrm C2 \<subseteq> nrm C2'" and
         brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
         by (rule da_weakenE) simp
-      have "PROP ?Hyp (In1r c2) (Norm s1) s2" .
+      note `PROP ?Hyp (In1r c2) (Norm s1) s2`
       with wt_c2 da_C2' G
       obtain nrmAss_C2': "?NormalAssigned s2 C2'" and
              brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and
@@ -3360,12 +3362,12 @@
       show ?thesis
         using that resAss_s2' by simp
     qed
-    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
-                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+    note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
+                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
     have s1_s2: "dom (locals s1) \<subseteq> dom (locals (store s2))"
     proof -  
-      have "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
-      thus ?thesis
+      from `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`
+      show ?thesis
         by (rule dom_locals_eval_mono_elim) simp
     qed
 
@@ -3455,7 +3457,7 @@
 	  by simp
 	moreover have "dom (locals (store ((Norm s1)::state))) 
                          \<subseteq> dom (locals (store s2))"
-	  by (rule dom_locals_eval_mono_elim)
+	  by (rule dom_locals_eval_mono_elim) (rule Fin.hyps)
 	ultimately have "Result \<in> dom (locals (store s2))"
 	  by - (rule subsetD,auto)
 	with res_s1 s3 show ?thesis
@@ -3473,7 +3475,7 @@
     ultimately show ?case by (intro conjI)
   next 
     case (Init C c s0 s3 s1 s2 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Init.hyps
     have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"
       apply (simp only: G) 
@@ -3483,8 +3485,7 @@
       apply (simp only: if_False )
       apply (elim conjE,intro conjI,assumption+,simp)
       done (* auto or simp alone always do too much *)
-    have "the (class G C) = c" .
-    with Init.prems 
+    from Init.prems and `the (class G C) = c`
     have c: "class G C = Some c"
       by (elim wt_elim_cases) auto
     from Init.prems obtain
@@ -3529,7 +3530,7 @@
     qed
   next 
     case (NewC s0 C s1 a s2 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from NewC.prems
     obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"
               "brk A = (\<lambda> l. UNIV)"
@@ -3540,10 +3541,10 @@
     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"
     proof -
       have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
-        by (rule dom_locals_eval_mono_elim)
+        by (rule dom_locals_eval_mono_elim) (rule NewC.hyps)
       also
       have "\<dots> \<subseteq> dom (locals (store s2))"
-        by (rule dom_locals_halloc_mono)
+        by (rule dom_locals_halloc_mono) (rule NewC.hyps)
       finally show ?thesis .
     qed
     with A have "?NormalAssigned s2 A"
@@ -3553,7 +3554,7 @@
       fix j have "abrupt s2 \<noteq> Some (Jump j)"
       proof -
         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
-	  by (simp only: G) (rule eval.NewC)
+	  unfolding G by (rule eval.NewC NewC.hyps)+
         from NewC.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -3569,7 +3570,7 @@
     ultimately show ?case by (intro conjI)
   next
     case (NewA s0 elT s1 e i s2 a s3 Env T A) 
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from NewA.prems obtain
       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
       by (elim da_elim_cases)
@@ -3577,15 +3578,15 @@
       wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
       wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
       by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
-    have halloc:"G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3".
+    note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3`
     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
-      by (rule dom_locals_eval_mono_elim)
+      by (rule dom_locals_eval_mono_elim) (rule NewA.hyps)
     with da_e obtain A' where
                 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" 
         and  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
         and  brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"
       by (rule da_weakenE) simp
-    have "PROP ?Hyp (In1l e) s1 s2" .
+    note `PROP ?Hyp (In1l e) s1 s2`
     with wt_size da_e' G obtain 
       nrmAss_A': "?NormalAssigned s2 A'" and
       brkAss_A': "?BreakAssigned s1 s2 A'"
@@ -3596,7 +3597,7 @@
              \<subseteq> dom (locals (store (abupd (check_neg i) s2)))"
         by (simp)
       also have "\<dots> \<subseteq> dom (locals (store s3))"
-        by (rule dom_locals_halloc_mono)
+        by (rule dom_locals_halloc_mono) (rule NewA.hyps)
       finally show ?thesis .
     qed 
     have "?NormalAssigned s3 A"
@@ -3618,7 +3619,7 @@
       fix j have "abrupt s3 \<noteq> Some (Jump j)"
       proof -
         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"
-	  by (simp only: G) (rule eval.NewA)
+	  unfolding G by (rule eval.NewA NewA.hyps)+
         from NewA.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -3634,19 +3635,19 @@
     ultimately show ?case by (intro conjI)
   next
     case (Cast s0 e v s1 s2 cT Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Cast.prems obtain
       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
       by (elim da_elim_cases)
     from Cast.prems obtain eT where
       wt_e: "Env\<turnstile>e\<Colon>-eT"
       by (elim wt_elim_cases) 
-    have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+    note `PROP ?Hyp (In1l e) (Norm s0) s1`
     with wt_e da_e G obtain 
       nrmAss_A: "?NormalAssigned s1 A" and
       brkAss_A: "?BreakAssigned (Norm s0) s1 A"
       by simp
-    have s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .
+    note s2 = `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
     hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
       by simp
     have "?NormalAssigned s2 A"
@@ -3663,7 +3664,7 @@
       fix j have "abrupt s2 \<noteq> Some (Jump j)"
       proof -
         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"
-	  by (simp only: G) (rule eval.Cast)
+	  unfolding G by (rule eval.Cast Cast.hyps)+
         from Cast.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -3679,14 +3680,14 @@
     ultimately show ?case by (intro conjI)
   next
     case (Inst s0 e v s1 b iT Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Inst.prems obtain
       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
       by (elim da_elim_cases)
     from Inst.prems obtain eT where
       wt_e: "Env\<turnstile>e\<Colon>-eT"
       by (elim wt_elim_cases) 
-    have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+    note `PROP ?Hyp (In1l e) (Norm s0) s1`
     with wt_e da_e G obtain 
       "?NormalAssigned s1 A" and
       "?BreakAssigned (Norm s0) s1 A" and
@@ -3701,14 +3702,14 @@
     thus ?case by simp
   next
     case (UnOp s0 e v s1 unop Env T A)
-     have G: "prg Env = G" .
+    note G = `prg Env = G`
     from UnOp.prems obtain
       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
       by (elim da_elim_cases)
     from UnOp.prems obtain eT where
       wt_e: "Env\<turnstile>e\<Colon>-eT"
       by (elim wt_elim_cases) 
-    have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+    note `PROP ?Hyp (In1l e) (Norm s0) s1`
     with wt_e da_e G obtain 
       "?NormalAssigned s1 A" and
       "?BreakAssigned (Norm s0) s1 A" and
@@ -3717,19 +3718,19 @@
     thus ?case by (intro conjI)
   next
     case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A)
-    have G: "prg Env = G". 
+    note G = `prg Env = G`
     from BinOp.hyps 
     have 
-     eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
+      eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
       by (simp only: G) (rule eval.BinOp)
     have s0_s1: "dom (locals (store ((Norm s0)::state))) 
                   \<subseteq> dom (locals (store s1))"
-      by (rule dom_locals_eval_mono_elim)
+      by (rule dom_locals_eval_mono_elim) (rule BinOp)
     also have s1_s2: "dom (locals (store s1)) \<subseteq>  dom (locals (store s2))"
-      by (rule dom_locals_eval_mono_elim)
+      by (rule dom_locals_eval_mono_elim) (rule BinOp)
     finally 
     have s0_s2: "dom (locals (store ((Norm s0)::state))) 
-                  \<subseteq> dom (locals (store s2))" . 
+                  \<subseteq> dom (locals (store s2))" .
     from BinOp.prems obtain e1T e2T
       where wt_e1: "Env\<turnstile>e1\<Colon>-e1T" 
        and  wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
@@ -3740,7 +3741,7 @@
     proof 
       assume normal_s2: "normal s2"
       have   normal_s1: "normal s1"
-        by (rule eval_no_abrupt_lemma [rule_format])
+        by (rule eval_no_abrupt_lemma [rule_format]) (rule BinOp.hyps, rule normal_s2)
       show "nrm A \<subseteq> dom (locals (store s2))"
       proof (cases "binop=CondAnd")
         case True
@@ -3832,7 +3833,7 @@
             where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"  
              and  da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"
             by (elim da_elim_cases) (simp_all add: notAndOr)
-          have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
+          note `PROP ?Hyp (In1l e1) (Norm s0) s1`
           with wt_e1 da_e1 G normal_s1
           obtain "?NormalAssigned s1 E1"  
             by simp
@@ -3883,20 +3884,21 @@
       from Acc.prems
       have "nrm A = dom (locals (store ((Norm s0)::state)))"
         by (simp only: vn) (elim da_elim_cases,simp_all)
-      moreover have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
-      hence "s1=Norm s0"
+      moreover
+      from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
+      have "s1=Norm s0"
         by (simp only: vn) (elim eval_elim_cases,simp)
       ultimately show ?thesis by simp
     next
       case False
-      have G: "prg Env = G" .
+      note G = `prg Env = G`
       from False Acc.prems
       have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"
         by (elim da_elim_cases) simp_all 
       from Acc.prems obtain vT where
         wt_v: "Env\<turnstile>v\<Colon>=vT"
         by (elim wt_elim_cases) 
-      have "PROP ?Hyp (In2 v) (Norm s0) s1" .
+      note `PROP ?Hyp (In2 v) (Norm s0) s1`
       with wt_v da_v G obtain 
         "?NormalAssigned s1 A" and
         "?BreakAssigned (Norm s0) s1 A" and
@@ -3906,7 +3908,7 @@
     qed
   next
     case (Ass s0 var w upd s1 e v s2 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Ass.prems obtain varT eT where
       wt_var: "Env\<turnstile>var\<Colon>=varT" and
       wt_e:   "Env\<turnstile>e\<Colon>-eT"
@@ -3920,9 +3922,9 @@
       have normal_s2: "normal s2"
         by (cases s2) (simp add: assign_def Let_def)
       hence normal_s1: "normal s1"
-        by - (rule eval_no_abrupt_lemma [rule_format])
-      have hyp_var: "PROP ?Hyp (In2 var) (Norm s0) s1" .
-      have hyp_e: "PROP ?Hyp (In1l e) s1 s2" .
+        by - (rule eval_no_abrupt_lemma [rule_format], rule Ass.hyps)
+      note hyp_var = `PROP ?Hyp (In2 var) (Norm s0) s1`
+      note hyp_e = `PROP ?Hyp (In1l e) s1 s2`
       show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"
       proof (cases "\<exists> vn. var = LVar vn")
 	case True
@@ -3937,9 +3939,9 @@
 	proof -
 	  have "dom (locals (store ((Norm s0)::state))) 
                   \<subseteq> dom (locals (store s1))"
-	    by (rule dom_locals_eval_mono_elim)
-	  with da_e show ?thesis
-	    by (rule da_weakenE)
+	    by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
+	  with da_e show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	from G eval_var vn 
 	have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1" 
@@ -4004,7 +4006,7 @@
       fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"
       proof -
         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"
-          by (simp only: G) (rule eval.Ass)
+          by (simp only: G) (rule eval.Ass Ass.hyps)+
         from Ass.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -4020,7 +4022,7 @@
     ultimately show ?case by (intro conjI)
   next
     case (Cond s0 e0 b s1 e1 e2 v s2 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     have "?NormalAssigned s2 A"
     proof 
       assume normal_s2: "normal s2"
@@ -4033,7 +4035,7 @@
                                  assigns_if False (e0 ? e1 : e2))"
           by (elim da_elim_cases) simp_all
         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"
-          by (simp only: G) (rule eval.Cond)
+          unfolding G by (rule eval.Cond Cond.hyps)+
         from eval 
         have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"
           by (rule dom_locals_eval_mono_elim)
@@ -4075,10 +4077,11 @@
           by (elim wt_elim_cases)
         have s0_s1: "dom (locals (store ((Norm s0)::state))) 
                        \<subseteq> dom (locals (store s1))"
-          by (rule dom_locals_eval_mono_elim)
-        have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" by (simp only: G)
+          by (rule dom_locals_eval_mono_elim) (rule Cond.hyps)
+        have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
+	  unfolding G by (rule Cond.hyps)
         have normal_s1: "normal s1"
-          by (rule eval_no_abrupt_lemma [rule_format])
+          by (rule eval_no_abrupt_lemma [rule_format]) (rule Cond.hyps, rule normal_s2)
         show ?thesis
         proof (cases "the_Bool b")
           case True
@@ -4126,7 +4129,7 @@
       fix j have "abrupt s2 \<noteq> Some (Jump j)"
       proof -
         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
-          by (simp only: G) (rule eval.Cond)
+          unfolding G by (rule eval.Cond Cond.hyps)+
         from Cond.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -4142,7 +4145,7 @@
   next
     case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
            Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     have "?NormalAssigned (restore_lvars s2 s4) A"
     proof 
       assume normal_restore_lvars: "normal (restore_lvars s2 s4)"
@@ -4156,23 +4159,23 @@
              wt_e: "Env\<turnstile>e\<Colon>-eT" and
           wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
           by (elim wt_elim_cases)
-        have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2" .
-        have s3': "s3' = check_method_access G accC statT mode 
-                                           \<lparr>name=mn,parTs=pTs\<rparr> a s3" .
+        note s3 = `s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2`
+        note s3' = `s3' = check_method_access G accC statT mode 
+                                           \<lparr>name=mn,parTs=pTs\<rparr> a s3`
         have normal_s2: "normal s2"
         proof -
           from normal_restore_lvars have "normal s4"
             by simp
           then have "normal s3'"
-            by - (rule eval_no_abrupt_lemma [rule_format])
+            by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
           with s3' have "normal s3"
             by (cases s3) (simp add: check_method_access_def Let_def)
           with s3 show "normal s2"
             by (cases s2) (simp add: init_lvars_def Let_def)
         qed
         then have normal_s1: "normal s1"
-          by  - (rule eval_no_abrupt_lemma [rule_format])
-        have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+          by  - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
+        note `PROP ?Hyp (In1l e) (Norm s0) s1`
         with da_e wt_e G normal_s1
         have "nrm E \<subseteq> dom (locals (store s1))"
           by simp
@@ -4180,7 +4183,7 @@
           da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
           by (rule da_weakenE) iprover
-        have "PROP ?Hyp (In3 args) s1 s2" .
+        note `PROP ?Hyp (In3 args) s1 s2`
         with da_args' wt_args G normal_s2
         have "nrm A' \<subseteq> dom (locals (store s2))"
           by simp
@@ -4197,7 +4200,7 @@
       proof -
         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v
                             \<rightarrow> (restore_lvars s2 s4)"
-          by (simp only: G) (rule eval.Call)
+          unfolding G by (rule eval.Call Call)+
         from Call.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -4214,7 +4217,7 @@
     ultimately show ?case by (intro conjI)
   next
     case (Methd s0 D sig v s1 Env T A)
-    have G: "prg Env = G". 
+    note G = `prg Env = G`
     from Methd.prems obtain m where
        m:      "methd (prg Env) D sig = Some m" and
        da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state)))) 
@@ -4224,7 +4227,7 @@
       isCls: "is_class (prg Env) D" and
       wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"
       by - (erule wt_elim_cases,simp)
-    have "PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1" .
+    note `PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1`
     moreover
     from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"
       using isCls m G by (simp add: body_def2)
@@ -4236,13 +4239,13 @@
       using G by simp
   next
     case (Body s0 D s1 c s2 s3 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     from Body.prems 
     have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"
       by (elim da_elim_cases) simp
     have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
                         \<rightarrow>abupd (absorb Ret) s3"
-      by (simp only: G) (rule eval.Body)
+      unfolding G by (rule eval.Body Body.hyps)+
     hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
       by  (simp only: nrm_A) (rule dom_locals_eval_mono_elim)
     hence "?NormalAssigned (abupd (absorb Ret) s3) A"
@@ -4262,14 +4265,14 @@
     thus ?case by simp
   next
     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     have "?NormalAssigned s3 A"
     proof 
       assume normal_s3: "normal s3"
       show "nrm A \<subseteq> dom (locals (store s3))"
       proof -
-        have fvar: "(v, s2') = fvar statDeclC stat fn a s2" and
-               s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
+        note fvar = `(v, s2') = fvar statDeclC stat fn a s2` and
+          s3 = `s3 = check_field_access G accC statDeclC fn stat a s2'`
         from FVar.prems
         have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
           by (elim da_elim_cases)
@@ -4278,7 +4281,7 @@
           by (elim wt_elim_cases)
         have "(dom (locals (store ((Norm s0)::state)))) 
                \<subseteq> dom (locals (store s1))"
-          by (rule dom_locals_eval_mono_elim)
+          by (rule dom_locals_eval_mono_elim) (rule FVar.hyps)
         with da_e obtain A' where
           da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
@@ -4292,7 +4295,7 @@
           show "normal s2"
             by (cases s2) (simp add: fvar_def2)
         qed
-        have "PROP ?Hyp (In1l e) s1 s2" . 
+        note `PROP ?Hyp (In1l e) s1 s2`
         with da_e' wt_e G normal_s2
         have "nrm A' \<subseteq> dom (locals (store s2))"
           by simp
@@ -4318,7 +4321,7 @@
         obtain w upd where v: "(w,upd)=v"
           by (cases v) auto
         have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"
-          by (simp only: G v) (rule eval.FVar)
+          by (simp only: G v) (rule eval.FVar FVar.hyps)+
         from FVar.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -4334,13 +4337,13 @@
     ultimately show ?case by (intro conjI)
   next
     case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     have "?NormalAssigned s2' A"
     proof 
       assume normal_s2': "normal s2'"
       show "nrm A \<subseteq> dom (locals (store s2'))"
       proof -
-        have avar: "(v, s2') = avar G i a s2" .
+        note avar = `(v, s2') = avar G i a s2`
         from AVar.prems obtain E1 where
           da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and
           da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A" 
@@ -4353,15 +4356,15 @@
         have normal_s2: "normal s2"
           by (cases s2) (simp add: avar_def2)
         hence "normal s1"
-          by - (rule eval_no_abrupt_lemma [rule_format])
-        moreover have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
+          by - (rule eval_no_abrupt_lemma [rule_format], rule AVar, rule normal_s2)
+        moreover note `PROP ?Hyp (In1l e1) (Norm s0) s1`
         ultimately have "nrm E1 \<subseteq> dom (locals (store s1))" 
           using da_e1 wt_e1 G by simp
         with da_e2 obtain A' where
           da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
           by (rule da_weakenE) iprover
-        have "PROP ?Hyp (In1l e2) s1 s2" .
+        note `PROP ?Hyp (In1l e2) s1 s2`
         with da_e2' wt_e2 G normal_s2
         have "nrm A' \<subseteq> dom (locals (store s2))"
           by simp
@@ -4384,7 +4387,7 @@
         obtain w upd where v: "(w,upd)=v"
           by (cases v) auto
         have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"
-          by  (simp only: G v) (rule eval.AVar)
+          unfolding G v by (rule eval.AVar AVar.hyps)+
         from AVar.prems 
         obtain T' where  "T=Inl T'"
           by (elim wt_elim_cases) simp
@@ -4406,7 +4409,7 @@
     thus ?case by simp
   next 
     case (Cons s0 e v s1 es vs s2 Env T A)
-    have G: "prg Env = G" .
+    note G = `prg Env = G`
     have "?NormalAssigned s2 A"
     proof 
       assume normal_s2: "normal s2"
@@ -4421,15 +4424,15 @@
              wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"
           by (elim wt_elim_cases)
         have "normal s1"
-          by - (rule eval_no_abrupt_lemma [rule_format])
-        moreover have "PROP ?Hyp (In1l e) (Norm s0) s1" .
+          by - (rule eval_no_abrupt_lemma [rule_format], rule Cons.hyps, rule normal_s2)
+        moreover note `PROP ?Hyp (In1l e) (Norm s0) s1`
         ultimately have "nrm E \<subseteq> dom (locals (store s1))" 
           using da_e wt_e G by simp
         with da_es obtain A' where
           da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
           by (rule da_weakenE) iprover
-        have "PROP ?Hyp (In3 es) s1 s2" .
+        note `PROP ?Hyp (In3 es) s1 s2`
         with da_es' wt_es G normal_s2
         have "nrm A' \<subseteq> dom (locals (store s2))"
           by simp
@@ -4442,7 +4445,7 @@
       fix j have "abrupt s2 \<noteq> Some (Jump j)"
       proof -
         have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"
-          by (simp only: G) (rule eval.Cons)
+          unfolding G by (rule eval.Cons Cons.hyps)+
         from Cons.prems 
         obtain T' where  "T=Inr T'"
           by (elim wt_elim_cases) simp
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/Evaln.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -410,7 +410,7 @@
 using evaln 
 proof (induct)
   case (Loop s0 e n b s1 c s2 l s3)
-  have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
+  note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
   moreover
   have "if the_Bool b
         then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
@@ -420,16 +420,16 @@
   ultimately show ?case by (rule eval.Loop)
 next
   case (Try s0 c1 n s1 s2 C vn c2 s3)
-  have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
+  note `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   moreover
-  have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
+  note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
   moreover
   have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
     using Try.hyps by simp
   ultimately show ?case by (rule eval.Try)
 next
   case (Init C c s0 s3 n s1 s2)
-  have "the (class G C) = c".
+  note `the (class G C) = c`
   moreover
   have "if inited C (globs s0) 
            then s3 = Norm s0
@@ -600,7 +600,7 @@
     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
     by (iprover)
   moreover 
-  have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
+  note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
   moreover
   from Try.hyps obtain n2 where
     "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
@@ -616,9 +616,9 @@
     "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
     by iprover
   moreover
-  have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
-                     then (x1, s1)
-                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
+  note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) 
+                   then (x1, s1)
+                   else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
   ultimately 
   have 
     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
@@ -626,7 +626,7 @@
   then show ?case ..
 next
   case (Init C c s0 s3 s1 s2)
-  have     cls: "the (class G C) = c" .
+  note cls = `the (class G C) = c`
   moreover from Init.hyps obtain n where
       "if inited C (globs s0) then s3 = Norm s0
        else (G\<turnstile>Norm (init_class_obj G C s0)
@@ -653,7 +653,7 @@
     "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
     by (iprover)
   moreover
-  have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
+  note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
     by (blast intro: evaln.NewA dest: evaln_max2)
@@ -664,7 +664,7 @@
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
     by (iprover)
   moreover 
-  have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
+  note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1`
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
     by (rule evaln.Cast)
@@ -675,7 +675,7 @@
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
     by (iprover)
   moreover 
-  have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
+  note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)`
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
     by (rule evaln.Inst)
@@ -745,12 +745,12 @@
     "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
     by iprover
   moreover
-  have "invDeclC = invocation_declclass G mode (store s2) a' statT 
-                       \<lparr>name=mn,parTs=pTs'\<rparr>" .
+  note `invDeclC = invocation_declclass G mode (store s2) a' statT 
+                       \<lparr>name=mn,parTs=pTs'\<rparr>`
   moreover
-  have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
+  note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2`
   moreover
-  have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
+  note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3`
   moreover 
   from Call.hyps
   obtain m where 
@@ -776,10 +776,10 @@
     evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
     by (iprover)
   moreover
-  have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
+  note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
                      fst s2 = Some (Jump (Cont l))
-                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
-                 else s2)".
+              then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
+              else s2)`
   ultimately
   have
      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
@@ -799,8 +799,8 @@
     "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
     by iprover
   moreover
-  have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
-       "(v, s2') = fvar statDeclC stat fn a s2" .
+  note `s3 = check_field_access G accC statDeclC fn stat a s2'`
+    and `(v, s2') = fvar statDeclC stat fn a s2`
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
     by (iprover intro: evaln.FVar dest: evaln_max2)
@@ -812,7 +812,7 @@
     "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
     by iprover
   moreover 
-  have "(v, s2') = avar G i a s2" .
+  note `(v, s2') = avar G i a s2`
   ultimately 
   have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
     by (blast intro!: evaln.AVar dest: evaln_max2)
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -724,7 +724,7 @@
 proof -
   assume error_free: "error_free state"
   obtain a s where "state=(a,s)"
-    by (cases state) simp
+    by (cases state)
   with error_free
   show ?thesis
     by (cases a) auto
@@ -792,7 +792,7 @@
 proof -
   assume error_free: "error_free state"
   obtain a s where "state=(a,s)"
-    by (cases state) simp
+    by (cases state)
   with error_free
   show ?thesis
     by (cases a) auto
@@ -991,7 +991,7 @@
   moreover
   from f subclseq
   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
-    by (auto intro!: static_to_dynamic_accessible_from 
+    by (auto intro!: static_to_dynamic_accessible_from wf
                dest: accfield_accessibleD)
   ultimately show ?thesis
     by blast
@@ -1182,8 +1182,8 @@
   case Nil thus ?case by simp
 next
   case (Cons p ps tab qs)
-  have "length (p#ps) = length qs" .
-  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
+  from `length (p#ps) = length qs`
+  obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
     by (rule Cons.hyps)
@@ -1198,8 +1198,8 @@
   case Nil thus ?case by simp
 next
   case (Cons p ps tab qs x y)
-  have "length (p#ps) = length qs" .
-  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
+  from `length (p#ps) = length qs`
+  obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
     by (cases qs) auto
   from eq_length 
   have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
@@ -1228,7 +1228,8 @@
   show ?case
   proof (cases ys)
     case Nil
-    thus ?thesis by simp
+    with Hyps
+    show ?thesis by simp
   next
     case (Cons y ys')
     have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
@@ -1290,14 +1291,14 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs tab ys z)
-  have z: "tab vn = Some z" .
+  note z = `tab vn = Some z`
   show ?case
   proof (cases ys)
     case Nil
     with z show ?thesis by simp
   next
     case (Cons y ys')
-    have ys: "ys = y#ys'".
+    note ys = `ys = y#ys'`
     from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
       by (rule map_upd_Some_expand [of tab,elim_format]) blast
     hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
@@ -1332,14 +1333,14 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs tab tab' ys z)
-  have some: "(tab(x # xs[\<mapsto>]ys)) vn = Some z" .
-  have tab_not_z: "tab vn \<noteq> Some z".
+  note some = `(tab(x # xs[\<mapsto>]ys)) vn = Some z`
+  note tab_not_z = `tab vn \<noteq> Some z`
   show ?case
-  proof (cases "ys")
+  proof (cases ys)
     case Nil with some tab_not_z show ?thesis by simp
   next
     case (Cons y tl)
-    have ys: "ys = y#tl".
+    note ys = `ys = y#tl`
     show ?thesis
     proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
       case True
@@ -1424,15 +1425,15 @@
   case Nil thus ?case by simp
 next
   case (Cons x xs tab tab' ys)
-  have tab_vn: "(tab(x # xs[\<mapsto>]ys)) vn = Some el".
-  have tab'_vn: "(tab'(x # xs[\<mapsto>]ys)) vn = None".
+  note tab_vn = `(tab(x # xs[\<mapsto>]ys)) vn = Some el`
+  note tab'_vn = `(tab'(x # xs[\<mapsto>]ys)) vn = None`
   show ?case
   proof (cases ys)
     case Nil
     with tab_vn show ?thesis by simp
   next
     case (Cons y tl)
-    have ys: "ys=y#tl".
+    note ys = `ys=y#tl`
     with tab_vn tab'_vn 
     have "(tab(x\<mapsto>y)) vn = Some el"
       by - (rule Cons.hyps,auto)
@@ -1509,7 +1510,7 @@
 next
   case (Cons x xs tab ys)
   note Hyp = Cons.hyps
-  have len: "length (x#xs)=length ys".
+  note len = `length (x#xs)=length ys`
   show ?case
   proof (cases ys)
     case Nil with len show ?thesis by simp
@@ -1740,30 +1741,30 @@
                      ?ErrorFree s0 s1")
   proof (induct)
     case (Abrupt xc s t L accC T A) 
-    have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
-    then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
+    from `(Some xc, s)\<Colon>\<preceq>(G,L)`
+    show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
       (normal (Some xc, s) 
       \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
       (error_free (Some xc, s) = error_free (Some xc, s))"
-      by (simp)
+      by simp
   next
     case (Skip s L accC T A)
-    have "Norm s\<Colon>\<preceq>(G, L)" and  
-           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
-    then show "Norm s\<Colon>\<preceq>(G, L) \<and>
+    from `Norm s\<Colon>\<preceq>(G, L)` and
+      `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T`
+    show "Norm s\<Colon>\<preceq>(G, L) \<and>
               (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
               (error_free (Norm s) = error_free (Norm s))"
-      by (simp)
+      by simp
   next
     case (Expr s0 e v s1 L accC T A)
-    have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
-    have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
     moreover
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T`
     then obtain eT 
       where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
-      by (rule wt_elim_cases) (blast)
+      by (rule wt_elim_cases) blast
     moreover
     from Expr.prems obtain E where
       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1l e\<guillemotright>E"
@@ -1778,12 +1779,12 @@
       by (simp)
   next
     case (Lab s0 c s1 l L accC T A)
-    have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
     moreover
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T`
     then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
-      by (rule wt_elim_cases) (blast)
+      by (rule wt_elim_cases) blast
     moreover from Lab.prems obtain C where
      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1r c\<guillemotright>C"
       by (elim da_elim_cases) simp
@@ -1801,15 +1802,15 @@
       by (simp)
   next
     case (Comp s0 c1 s1 c2 s2 L accC T A)
-    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
-    have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
-    have  hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
-    have  hyp_c2: "PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T" .
+    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+    note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
+    note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
+    note hyp_c2 = `PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T`
     then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
                 wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
-      by (rule wt_elim_cases) (blast)
+      by (rule wt_elim_cases) blast
     from Comp.prems
     obtain C1 C2
       where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
@@ -1836,8 +1837,8 @@
 	from eval_c1 wt_c1 da_c1 wf True
 	have "nrm C1 \<subseteq> dom (locals (store s1))"
 	  by (cases rule: da_good_approxE') iprover
-	with da_c2 show ?thesis
-	  by (rule da_weakenE)
+	with da_c2 show thesis
+	  by (rule da_weakenE) (rule that)
       qed
       with conf_s1 wt_c2 
       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
@@ -1847,13 +1848,13 @@
     qed
   next
     case (If s0 e b s1 c1 c2 s2 L accC T A)
-    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
-    have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
-    have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
-    have hyp_then_else: 
-            "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
+    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
+    note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
+    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
+    note hyp_then_else =
+      `PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T`
     then obtain 
               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
@@ -1902,8 +1903,8 @@
 	have "dom (locals (store ((Norm s0)::state))) 
                 \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
 	  by (rule Un_least)
-	with da_then_else show ?thesis
-	  by (rule da_weakenE)
+	with da_then_else show thesis
+	  by (rule da_weakenE) (rule that)
       qed
       with conf_s1 wt_then_else  
       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
@@ -1922,15 +1923,15 @@
        *}
   next
     case (Loop s0 e b s1 c s2 l s3 L accC T A)
-    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
-    have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
+    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
+    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
-      by (rule wt_elim_cases) (blast)
-    have da:"\<lparr>prg=G, cls=accC, lcl=L\<rparr>
-            \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A".
+      by (rule wt_elim_cases) blast
+    note da = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
+            \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A`
     then
     obtain E C where
       da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
@@ -1939,7 +1940,7 @@
               \<turnstile> (dom (locals (store ((Norm s0)::state))) 
                    \<union> assigns_if True e) \<guillemotright>In1r c\<guillemotright> C" 
       by (rule da_elim_cases) simp
-    from conf_s0 wt_e da_e 
+    from conf_s0 wt_e da_e
     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
       by (rule hyp_e [elim_format]) simp
     show "s3\<Colon>\<preceq>(G, L) \<and>
@@ -1978,8 +1979,8 @@
 	  have "dom (locals (store ((Norm s0)::state))) 
                  \<union> assigns_if True e \<subseteq> dom (locals (store s1))"
 	    by (rule Un_least)
-	  with da_c show ?thesis
-	    by (rule da_weakenE)
+	  with da_c show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	with conf_s1 wt_c  
 	obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
@@ -2004,8 +2005,8 @@
 	    by simp
 	  finally
           have "dom (locals (store ((Norm s0)::state))) \<subseteq> \<dots>" .
-	  with da show ?thesis
-	    by (rule da_weakenE)
+	  with da show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
 	  by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
@@ -2053,7 +2054,7 @@
     qed
   next
     case (Jmp s j L accC T A)
-    have "Norm s\<Colon>\<preceq>(G, L)" .
+    note `Norm s\<Colon>\<preceq>(G, L)`
     moreover
     from Jmp.prems 
     have "j=Ret \<longrightarrow> Result \<in> dom (locals (store ((Norm s)::state)))"
@@ -2067,10 +2068,10 @@
       by simp
   next
     case (Throw s0 e a s1 L accC T A)
-    have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
-    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T" .
+    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T`
     then obtain tn 
       where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
             throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
@@ -2095,11 +2096,11 @@
       by simp
   next
     case (Try s0 c1 s1 s2 catchC vn c2 s3 L accC T A)
-    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
-    have sx_alloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
-    have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
-    have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
+    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+    note sx_alloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
+    note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T`
     then obtain 
       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
@@ -2177,8 +2178,8 @@
 	  have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
                   \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
           proof -
-            have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
-            hence "dom (locals (store ((Norm s0)::state))) 
+            from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+            have "dom (locals (store ((Norm s0)::state))) 
                     \<subseteq> dom (locals (store s1))"
               by (rule dom_locals_eval_mono_elim)
             also
@@ -2194,8 +2195,8 @@
             ultimately show ?thesis
               by (rule Un_least)
           qed
-	  with da_c2 show ?thesis
-	    by (rule da_weakenE)
+	  with da_c2 show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	ultimately
 	obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
@@ -2212,20 +2213,20 @@
     qed
   next
     case (Fin s0 c1 x1 s1 c2 s2 s3 L accC T A)
-    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
-    have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
-    have s3: "s3= (if \<exists>err. x1 = Some (Error err) 
+    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)`
+    note eval_c2 = `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`
+    note s3 = `s3 = (if \<exists>err. x1 = Some (Error err)
                      then (x1, s1)
-                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
-    have  hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
-    have  hyp_c2: "PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
+                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
+    note hyp_c1 = `PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>`
+    note hyp_c2 = `PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T`
     then obtain
       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
       by (rule wt_elim_cases) blast
-    from Fin.prems obtain C1 C2 where 
+    from Fin.prems obtain C1 C2 where
       da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and
       da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
@@ -2248,8 +2249,8 @@
       hence "dom (locals (store ((Norm s0)::state))) 
               \<subseteq> dom (locals (store ((Norm s1)::state)))"
 	by simp
-      with da_c2 show ?thesis
-	by (rule da_weakenE)
+      with da_c2 show thesis
+	by (rule da_weakenE) (rule that)
     qed
     ultimately
     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
@@ -2261,7 +2262,8 @@
           (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
           (error_free (Norm s0) = error_free s3)"
     proof (cases x1)
-      case None with conf_s2 s3' wt show ?thesis by auto
+      case None with conf_s2 s3' wt error_free_s2
+      show ?thesis by auto
     next
       case (Some x) 
       from eval_c2 have 
@@ -2281,12 +2283,12 @@
     qed
   next
     case (Init C c s0 s3 s1 s2 L accC T A)
-    have     cls: "the (class G C) = c" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
+    note cls = `the (class G C) = c`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T`
     with cls
     have cls_C: "class G C = Some c"
-      by - (erule wt_elim_cases,auto)
+      by - (erule wt_elim_cases, auto)
     show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
           (error_free (Norm s0) = error_free s3)"
     proof (cases "inited C (globs s0)")
@@ -2387,12 +2389,12 @@
     qed
   next
     case (NewC s0 C s1 a s2 L accC T A)
-    have         "G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1" .
-    have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
-    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    note `G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1`
+    note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
     moreover
-    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
+    note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T`
     then obtain is_cls_C: "is_class G C" and
                        T: "T=Inl (Class C)"
       by (rule wt_elim_cases) (auto dest: is_acc_classD)
@@ -2419,13 +2421,13 @@
       by auto
   next
     case (NewA s0 elT s1 e i s2 a s3 L accC T A)
-    have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1" .
-    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
-    have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
-    have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>" .
-    have hyp_size: "PROP ?TypeSafe s1 s2 (In1l e) (In1 i)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T" .
+    note eval_init = `G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1`
+    note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2`
+    note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
+    note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>`
+    note hyp_size = `PROP ?TypeSafe s1 s2 (In1l e) (In1 i)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T`
     then obtain
       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
@@ -2457,8 +2459,8 @@
                            simp add: init_comp_ty_def))
          (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
       qed
-      ultimately show ?thesis
-	by (rule hyp_init [elim_format]) auto
+      ultimately show thesis
+	by (rule hyp_init [elim_format]) (auto intro: that)
     qed 
     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
     proof -
@@ -2490,11 +2492,11 @@
       by simp
   next
     case (Cast s0 e v s1 s2 castT L accC T A)
-    have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
-    have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
-    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T" .
+    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+    note s2 = `s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1`
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T`
     then obtain eT
       where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
               eT: "G\<turnstile>eT\<preceq>? castT" and 
@@ -2536,8 +2538,8 @@
       by blast
   next
     case (Inst s0 e v s1 b instT L accC T A)
-    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
     from Inst.prems obtain eT
     where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-RefT eT"  and
              T: "T=Inl (PrimT Boolean)" 
@@ -2560,9 +2562,9 @@
                intro: conf_litval simp add: empty_dt_def)
   next
     case (UnOp s0 e v s1 unop L accC T A)
-    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T`
     then obtain eT
       where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
             wt_unop: "wt_unop unop eT" and
@@ -2587,15 +2589,15 @@
       by simp
   next
     case (BinOp s0 e1 v1 s1 binop e2 v2 s2 L accC T A)
-    have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" .
-    have eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
-                             else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
-    have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
-    have hyp_e2: "PROP ?TypeSafe       s1  s2 
+    note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1`
+    note eval_e2 = `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
+                             else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
+    note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)`
+    note hyp_e2 = `PROP ?TypeSafe       s1  s2 
                    (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
-                   (In1 v2)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
+                   (In1 v2)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T`
     then obtain e1T e2T where
          wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
          wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
@@ -2608,8 +2610,8 @@
       daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
       by (auto intro: da_Skip [simplified] assigned.select_convs)
-    have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
-                  \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A".
+    note da = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
+                  \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A`
     then obtain E1 where
       da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e1\<guillemotright> E1"
@@ -2703,8 +2705,8 @@
       by simp
   next
     case (Acc s0 v w upd s1 L accC T A)
-    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
     from Acc.prems obtain vT where
       wt_v: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>v\<Colon>=vT" and
          T: "T=Inl vT"
@@ -2712,7 +2714,7 @@
     from Acc.prems obtain V where
       da_v: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 v\<guillemotright> V"
-      by (cases "\<exists> n. v=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
+      by (cases "\<exists> n. v=LVar n") (insert da.LVar, auto elim!: da_elim_cases)
     {
       fix n assume lvar: "v=LVar n"
       have "locals (store s1) n \<noteq> None"
@@ -2723,8 +2725,8 @@
 	also
 	have "dom (locals s0) \<subseteq> dom (locals (store s1))"
 	proof -
-	  have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
-	  thus ?thesis
+	  from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
+	  show ?thesis
 	    by (rule dom_locals_eval_mono_elim) simp
 	qed
 	finally show ?thesis
@@ -2743,12 +2745,12 @@
       by simp
   next
     case (Ass s0 var w upd s1 e v s2 L accC T A)
-    have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1" .
-    have   eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
-    have  hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))" .
-    have    hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 v)" .
-    have  conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T" .
+    note eval_var = `G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1`
+    note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
+    note hyp_var = `PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))`
+    note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T`
     then obtain varT eT where
 	 wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
 	   wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
@@ -2790,8 +2792,8 @@
 	  from eval_var wt_var da_var wf normal_s1
 	  have "nrm V \<subseteq>  dom (locals (store s1))"
 	    by (cases rule: da_good_approxE') iprover
-	  with da_e show ?thesis
-	    by (rule da_weakenE) 
+	  with da_e show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	with conf_s1 wt_e 
 	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
@@ -2844,9 +2846,9 @@
       proof -
 	have "dom (locals (store ((Norm s0)::state))) 
                 \<subseteq> dom (locals (store (s1)))"
-	  by (rule dom_locals_eval_mono_elim)
-	with da_e show ?thesis
-	  by (rule da_weakenE)
+	  by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
+	with da_e show thesis
+	  by (rule da_weakenE) (rule that)
       qed
       from conf_s0 wt_var da_var 
       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
@@ -2900,13 +2902,13 @@
     qed
   next
     case (Cond s0 e0 b s1 e1 e2 v s2 L accC T A)
-    have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
-    have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
-    have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" .
-    have hyp_if: "PROP ?TypeSafe s1 s2 
-                       (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
+    note eval_e0 = `G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
+    note eval_e1_e2 = `G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2`
+    note hyp_e0 = `PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)`
+    note hyp_if = `PROP ?TypeSafe s1 s2
+                       (In1l (if the_Bool b then e1 else e2)) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T`
     then obtain T1 T2 statT where
       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
@@ -2994,24 +2996,24 @@
   next
     case (Call s0 e a s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC'
            v s4 L accC T A)
-    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
-    have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
-    have invDeclC: "invDeclC 
+    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
+    note eval_args = `G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2`
+    note invDeclC = `invDeclC 
                       = invocation_declclass G mode (store s2) a statT 
-                           \<lparr>name = mn, parTs = pTs'\<rparr>" .
-    have init_lvars: 
-           "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2".
-    have check: "s3' =
-       check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3" .
-    have eval_methd: 
-           "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
-    have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
-    have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
-    have hyp_methd: "PROP ?TypeSafe s3' s4 
-               (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
-                    \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
+                           \<lparr>name = mn, parTs = pTs'\<rparr>`
+    note init_lvars =
+      `s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2`
+    note check = `s3' =
+        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3`
+    note eval_methd =
+      `G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4`
+    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
+    note hyp_args = `PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)`
+    note hyp_methd = `PROP ?TypeSafe s3' s4 
+        (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
+        \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T`
     from wt obtain pTs statDeclT statM where
                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
@@ -3074,8 +3076,8 @@
 	from eval_e wt_e da_e wf normal_s1
 	have "nrm E \<subseteq>  dom (locals (store s1))"
 	  by (cases rule: da_good_approxE') iprover
-	with da_args show ?thesis
-	  by (rule da_weakenE) 
+	with da_args show thesis
+	  by (rule da_weakenE) (rule that)
       qed
       with conf_s1 wt_args 
       obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
@@ -3290,8 +3292,7 @@
 	      by (iprover intro: da.Body assigned.select_convs)
 	    from _ this [simplified]
 	    show ?thesis
-	      by (rule da.Methd [simplified,elim_format])
-	         (auto intro: dynM')
+	      by (rule da.Methd [simplified,elim_format]) (auto intro: dynM' that)
 	  qed
 	  ultimately obtain  
 	    conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
@@ -3337,10 +3338,10 @@
     qed
   next
     case (Methd s0 D sig v s1 L accC T A)
-    have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
-    have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
+    note `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
+    note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T`
     then obtain m bodyT where
       D: "is_class G D" and
       m: "methd G D sig = Some m" and
@@ -3362,12 +3363,12 @@
       by (auto simp add: Let_def body_def)
   next
     case (Body s0 D s1 c s2 s3 L accC T A)
-    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
-    have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
-    have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>" .
-    have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T" .
+    note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1`
+    note eval_c = `G\<turnstile>s1 \<midarrow>c\<rightarrow> s2`
+    note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>`
+    note hyp_c = `PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T`
     then obtain bodyT where
          iscls_D: "is_class G D" and
             wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
@@ -3399,7 +3400,7 @@
       have "(dom (locals (store ((Norm s0)::state)))) 
                      \<subseteq> (dom (locals (store s1)))"
 	by (rule dom_locals_eval_mono_elim)
-      with da_c show ?thesis by (rule da_weakenE)
+      with da_c show thesis by (rule da_weakenE) (rule that)
     qed
     from conf_s1 wt_c da_C' 
     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
@@ -3429,7 +3430,7 @@
                 (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
                         abrupt s2 = Some (Jump (Cont l))
                  then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
-      ultimately show ?thesis 
+      ultimately show ?thesis
 	by force
     qed
     moreover
@@ -3463,8 +3464,8 @@
       by (cases s2) (auto intro: conforms_locals)
   next
     case (LVar s vn L accC T)
-    have conf_s: "Norm s\<Colon>\<preceq>(G, L)" and 
-             wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T" .
+    note conf_s = `Norm s\<Colon>\<preceq>(G, L)` and
+      wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T`
     then obtain vnT where
       vnT: "L vn = Some vnT" and
         T: "T=Inl vnT"
@@ -3486,14 +3487,14 @@
       by (simp add: lvar_def) 
   next
     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC L accC' T A)
-    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
-    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
-    have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
-    have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
-    have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
-    have hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 a)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
+    note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1`
+    note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2`
+    note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
+    note check = `s3 = check_field_access G accC statDeclC fn stat a s2'`
+    note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>`
+    note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 a)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T`
     then obtain statC f where
                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
@@ -3529,8 +3530,8 @@
       have "(dom (locals (store ((Norm s0)::state)))) 
 	       \<subseteq> (dom (locals (store s1)))"
 	by (rule dom_locals_eval_mono_elim)
-      with da_e show ?thesis
-	by (rule da_weakenE)
+      with da_e show thesis
+	by (rule da_weakenE) (rule that)
     qed
     with conf_s1 wt_e 
     obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
@@ -3602,13 +3603,13 @@
       by auto
   next
     case (AVar s0 e1 a s1 e2 i s2 v s2' L accC T A)
-    have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1" .
-    have eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2" .
-    have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" .
-    have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)" .
-    have avar: "(v, s2') = avar G i a s2" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have wt:  "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T" .
+    note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1`
+    note eval_e2 = `G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2`
+    note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)`
+    note hyp_e2 = `PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)`
+    note avar = `(v, s2') = avar G i a s2`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T`
     then obtain elemT
        where wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
              wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
@@ -3702,12 +3703,12 @@
       by (auto elim!: wt_elim_cases)
   next
     case (Cons s0 e v s1 es vs s2 L accC T A)
-    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
-    have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .
-    have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
-    have hyp_es: "PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)" .
-    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
-    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T" .
+    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
+    note eval_es = `G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2`
+    note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
+    note hyp_es = `PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)`
+    note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
+    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T`
     then obtain eT esT where
        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
        wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
@@ -3740,8 +3741,8 @@
 	from eval_e wt_e da_e wf True
 	have "nrm E \<subseteq> dom (locals (store s1))"
 	  by (cases rule: da_good_approxE') iprover
-	with da_es show ?thesis
-	  by (rule da_weakenE)
+	with da_es show thesis
+	  by (rule da_weakenE) (rule that)
       qed
       with conf_s1 wt_es
       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
@@ -3758,7 +3759,7 @@
       ultimately show ?thesis using T by simp
     qed
   qed
-  then show ?thesis .
+  from this and conf_s0 wt da show ?thesis .
 qed
 
 text {* 
@@ -3938,8 +3939,8 @@
       by (rule lab)
   next
     case (Comp s0 c1 s1 c2 s2 L accC T A) 
-    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
-    have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
+    note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
+    note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
     from Comp.prems obtain 
       wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
       wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
@@ -3967,8 +3968,8 @@
 	  from eval_c1 wt_c1 da_c1 wf normal_s1
 	  have "nrm C1 \<subseteq> dom (locals (store s1))"
 	    by (cases rule: da_good_approxE') iprover
-	  with da_c2 show ?thesis
-	    by (rule da_weakenE)
+	  with da_c2 show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
 	  by (rule Comp.hyps)
@@ -3981,8 +3982,8 @@
       by (rule comp) iprover+
   next
     case (If s0 e b s1 c1 c2 s2 L accC T A)
-    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
-    have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
+    note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
+    note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
     from If.prems
     obtain 
               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
@@ -4023,8 +4024,8 @@
 	  have "dom (locals (store ((Norm s0)::state))) 
             \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
 	    by (rule Un_least)
-	  with da_then_else show ?thesis
-	    by (rule da_weakenE)
+	  with da_then_else show thesis
+	    by (rule da_weakenE) (rule that)
 	qed
 	with wt_then_else
 	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
diff -r 23a8345f89f5 -r 50c5b0912a0c src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Wed Jun 13 00:01:38 2007 +0200
+++ b/src/HOL/Bali/WellForm.thy	Wed Jun 13 00:01:41 2007 +0200
@@ -1992,11 +1992,11 @@
     show "?thesis m d" 
     proof (cases "?newMethods")
       case None
-      from None clsC nObj ws m declC hyp  
-      show "?thesis" by (auto simp add: methd_rec)
+      from None clsC nObj ws m declC
+      show "?thesis" by (auto simp add: methd_rec) (rule hyp)
     next
       case Some
-      from Some clsC nObj ws m declC hyp  
+      from Some clsC nObj ws m declC
       show "?thesis" 
 	by (auto simp add: methd_rec
                      dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
@@ -2665,7 +2665,7 @@
       with neq show ?thesis 
 	by (contradiction)
     next
-      case Subcls show ?thesis .
+      case Subcls then show ?thesis .
     qed 
     moreover
     from stat_acc wf 
@@ -2920,8 +2920,8 @@
   show ?thesis
   proof (induct)
     case (Immediate m C)
-    have "G \<turnstile> m in C permits_acc_from accC" and "accmodi m = Private" .
-    then show ?case
+    from `G \<turnstile> m in C permits_acc_from accC` and `accmodi m = Private`
+    show ?case
       by (simp add: permits_acc_def)
   next
     case Overriding
@@ -2985,8 +2985,8 @@
   show ?thesis
   proof (induct)
     case (Immediate f C)
-    have "G \<turnstile> f in C permits_acc_from accC" and "accmodi f = Package" .
-    then show ?case
+    from `G \<turnstile> f in C permits_acc_from accC` and `accmodi f = Package`
+    show ?case
       by (simp add: permits_acc_def)
   next
     case Overriding
@@ -3009,7 +3009,7 @@
   show ?thesis
   proof (induct)
     case (Immediate f C)
-    have "G \<turnstile> f in C permits_acc_from accC" .
+    note `G \<turnstile> f in C permits_acc_from accC`
     moreover 
     assume "accmodi f = Protected" and  "is_field f" and "\<not> is_static f" and
            "pid (declclass f) \<noteq> pid accC"
@@ -3036,14 +3036,14 @@
     case (Immediate f C)
     assume "accmodi f = Protected" and  "is_field f" and "is_static f" and
            "pid (declclass f) \<noteq> pid accC"
-    moreover 
-    have "G \<turnstile> f in C permits_acc_from accC" .
+    moreover
+    note `G \<turnstile> f in C permits_acc_from accC`
     ultimately
     have "G\<turnstile> accC \<preceq>\<^sub>C declclass f"
       by (auto simp add: permits_acc_def)
     moreover
-    have "G \<turnstile> f member_in C" .
-    then have "G\<turnstile>C \<preceq>\<^sub>C declclass f"
+    from `G \<turnstile> f member_in C`
+    have "G\<turnstile>C \<preceq>\<^sub>C declclass f"
       by (rule member_in_class_relation)
     ultimately show ?case
       by blast
@@ -3053,4 +3053,4 @@
   qed
 qed
 
-end
\ No newline at end of file
+end