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: