src/HOL/Bali/WellForm.thy

     and   nObj: "C \<noteq> Object"
     let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig"
     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)
     qed
   qed

       have "newM=statM" 
 	by (auto simp add: dynmethd_C_C)
       with neq show ?thesis 
 	by (contradiction)
     next
-      case Subcls show ?thesis .
+      case Subcls then show ?thesis .
     qed 
     moreover
     from stat_acc wf 
     have "G\<turnstile>Methd sig statM in statC dyn_accessible_from accC"
       by (blast intro: static_to_dynamic_accessible_from)

 proof -
   from dyn_acc priv
   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
     then show ?case
       by (auto dest!: overrides_commonD)

 proof -
   from dyn_acc pack field
   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
     then show ?case by (simp add: is_field_def)
   qed

 proof -
   from dyn_acc prot field instance_field outside
   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"
     ultimately 
     show "G\<turnstile> C \<preceq>\<^sub>C accC"

   show ?thesis
   proof (induct)
     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
   next
     case Overriding