# HG changeset patch
# User wenzelm
# Date 1014666494 -3600
# Node ID 0c4fd7529467073f3913820d3ebf947b5202f360
# Parent  84eb6c75cfe352def4975811aec31e4922d13ea5
clarified syntax of ``long'' statements: fixes/assumes/shows;

diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/FOL/IFOL.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -126,7 +126,10 @@
 subsection {* Intuitionistic Reasoning *}
 
 lemma impE':
-  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
+  assumes 1: "P --> Q"
+    and 2: "Q ==> R"
+    and 3: "P --> Q ==> P"
+  shows R
 proof -
   from 3 and 1 have P .
   with 1 have Q by (rule impE)
@@ -134,13 +137,18 @@
 qed
 
 lemma allE':
-  (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
+  assumes 1: "ALL x. P(x)"
+    and 2: "P(x) ==> ALL x. P(x) ==> Q"
+  shows Q
 proof -
   from 1 have "P(x)" by (rule spec)
   from this and 1 show Q by (rule 2)
 qed
 
-lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
+lemma notE':
+  assumes 1: "~ P"
+    and 2: "~ P ==> P"
+  shows R
 proof -
   from 2 and 1 have P .
   with 1 show R by (rule notE)
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/AxSound.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -247,11 +247,11 @@
 done
 
 corollary evaln_type_sound:
-      (assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
-                  wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
-             conf_s0: "s0\<Colon>\<preceq>(G,L)" and
-                  wf: "wf_prog G"                         
-      ) "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
+  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
+             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
+        conf_s0: "s0\<Colon>\<preceq>(G,L)" and
+             wf: "wf_prog G"                         
+  shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
          (error_free s0 = error_free s1)"
 proof -
   from evaln wt conf_s0 wf
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/Decl.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -723,12 +723,12 @@
 qed
 
 lemma ws_interface_induct [consumes 2, case_names Step]:
- (assumes is_if_I: "is_iface G I" and 
+  assumes is_if_I: "is_iface G I" and 
                ws: "ws_prog G" and
           hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 
                             \<forall> J \<in> set (isuperIfs i).
                                  (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J\<rbrakk> \<Longrightarrow> P I"
- ) "P I"
+  shows "P I"
 proof -
   from is_if_I ws 
   show "P I"
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -1007,10 +1007,10 @@
             split: memberdecl.splits)
 
 lemma unique_member_of: 
- (assumes n: "G\<turnstile>n member_of C" and  
+  assumes n: "G\<turnstile>n member_of C" and  
           m: "G\<turnstile>m member_of C" and
        eqid: "memberid n = memberid m"
- ) "n=m"
+  shows "n=m"
 proof -
   from n m eqid  
   show "n=m"
@@ -1173,9 +1173,9 @@
 by (cases "accmodi m") (auto simp add: permits_acc_def)
 
 lemma dyn_accessible_from_static_declC: 
-  (assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
+  assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
            static: "is_static m"
-  ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
+  shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
 proof -
   from acc_C static
   show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
@@ -1304,11 +1304,11 @@
 by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
 
 lemma member_of_inheritance:
-  (assumes    m: "G\<turnstile>m member_of D" and 
+  assumes       m: "G\<turnstile>m member_of D" and
      subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
      subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and
                ws: "ws_prog G" 
-  ) "G\<turnstile>m member_of C"
+  shows "G\<turnstile>m member_of C"
 proof -
   from m subclseq_D_C subclseq_C_m
   show ?thesis
@@ -1352,13 +1352,13 @@
 qed
 
 lemma member_of_subcls:
-  (assumes    old: "G\<turnstile>old member_of C" and 
+  assumes     old: "G\<turnstile>old member_of C" and 
               new: "G\<turnstile>new member_of D" and
              eqid: "memberid new = memberid old" and
      subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
    subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and
                ws: "ws_prog G"
-  ) "G\<turnstile>D \<prec>\<^sub>C C"
+  shows "G\<turnstile>D \<prec>\<^sub>C C"
 proof -
   from old 
   have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
@@ -1423,10 +1423,10 @@
 
 
 lemma inherited_field_access: 
- (assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
+  assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
           is_field: "is_field membr" and 
           subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"
- ) "G\<turnstile>membr in dynC dyn_accessible_from accC"
+  shows "G\<turnstile>membr in dynC dyn_accessible_from accC"
 proof -
   from stat_acc is_field subclseq 
   show ?thesis
@@ -1437,11 +1437,11 @@
 qed
 
 lemma accessible_inheritance:
- (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
+  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
        member_dynC: "G\<turnstile>m member_of dynC" and
           dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)"
- ) "G\<turnstile>m of dynC accessible_from accC"
+  shows "G\<turnstile>m of dynC accessible_from accC"
 proof -
   from stat_acc
   have member_statC: "G\<turnstile>m member_of statC" 
@@ -1664,13 +1664,13 @@
 done
 
 lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
- (assumes im: "im \<in> imethds G I sig" and  
+  assumes im: "im \<in> imethds G I sig" and  
          ifI: "iface G I = Some i" and
           ws: "ws_prog G" and
      hyp_new:  "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig 
                 = Some im \<Longrightarrow> P" and
      hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
-  ) "P"
+  shows P
 proof -
   from ifI ws im hyp_new hyp_inh
   show "P"
@@ -1756,9 +1756,9 @@
 by (auto dest: methd_declC method_declared_inI)
 
 lemma member_methd:
- (assumes member_of: "G\<turnstile>Methd sig m member_of C" and
+  assumes member_of: "G\<turnstile>Methd sig m member_of C" and
                  ws: "ws_prog G"
- ) "methd G C sig = Some m"
+  shows "methd G C sig = Some m"
 proof -
   from member_of 
   have iscls_C: "is_class G C" 
@@ -2013,13 +2013,13 @@
 by (auto simp add: dynmethd_rec)
  
 lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
-  (assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
+  assumes      dynM: "dynmethd G statC dynC sig = Some dynM" and
         is_cls_dynC: "is_class G dynC" and
                  ws: "ws_prog G" and
          hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
        hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
                        G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
-   ) "P"
+  shows P
 proof -
   from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
   from clsDynC ws dynM hyp_static hyp_override
@@ -2037,13 +2037,12 @@
 qed
 
 lemma no_override_in_Object:
-  (assumes     dynM: "dynmethd G statC dynC sig = Some dynM" and
+  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
             is_cls_dynC: "is_class G dynC" and
                      ws: "ws_prog G" and
                   statM: "methd G statC sig = Some statM" and
          neq_dynM_statM: "dynM\<noteq>statM"
-   )
-   "dynC \<noteq> Object"
+  shows "dynC \<noteq> Object"
 proof -
   from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
   from clsDynC ws dynM statM neq_dynM_statM 
@@ -2063,7 +2062,7 @@
 
 lemma dynmethd_Some_rec_cases [consumes 3, 
                                case_names Static Override  Recursion]:
-(assumes     dynM: "dynmethd G statC dynC sig = Some dynM" and
+  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
                 clsDynC: "class G dynC = Some c" and
                      ws: "ws_prog G" and
              hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
@@ -2072,8 +2071,8 @@
                                      G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
 
           hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
-                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P" 
-  ) "P"
+                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
+  shows P
 proof -
   from clsDynC have "is_class G dynC" by simp
   note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
@@ -2139,12 +2138,12 @@
 qed
 
 lemma methd_Some_dynmethd_Some:
-  (assumes    statM: "methd G statC sig = Some statM" and 
+  assumes     statM: "methd G statC sig = Some statM" and
            subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
        is_cls_statC: "is_class G statC" and
                  ws: "ws_prog G"
-   ) "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
-   (is "?P dynC")
+  shows "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
+    (is "?P dynC")
 proof -
   from subclseq is_cls_statC 
   have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
@@ -2185,7 +2184,7 @@
 qed
 
 lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
-  (assumes    statM: "methd G statC sig = Some statM" and 
+  assumes     statM: "methd G statC sig = Some statM" and 
            subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
        is_cls_statC: "is_class G statC" and
                  ws: "ws_prog G" and
@@ -2193,7 +2192,7 @@
        hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
                                  dynM\<noteq>statM;
                            G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
-   ) "P"
+  shows P
 proof -
   from subclseq is_cls_statC 
   have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
@@ -2215,13 +2214,13 @@
 qed
 
 lemma ws_dynmethd:
-  (assumes statM: "methd G statC sig = Some statM" and
+  assumes  statM: "methd G statC sig = Some statM" and
         subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
     is_cls_statC: "is_class G statC" and
               ws: "ws_prog G"
-   )
-   "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
-            is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
+  shows
+    "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
+             is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
 proof - 
   from statM subclseq is_cls_statC ws
   show ?thesis
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/Evaln.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -324,12 +324,12 @@
 done
 
 lemma evaln_eval:  
- (assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
+  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
              wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
         conf_s0: "s0\<Colon>\<preceq>(G, L)" and
              wf: "wf_prog G" 
        
- )  "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
+  shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
 proof -
   from evaln 
   show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
@@ -477,8 +477,9 @@
   next
     case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT 
            v vs L accC T)
-    (* Repeats large parts of the type soundness proof. One should factor
-       out some lemmata about the relations and conformance of s2, s3 and s3'*)
+    txt {* Repeats large parts of the type soundness proof. One should factor
+      out some lemmata about the relations and conformance of @{text
+      s2}, @{text s3} and @{text s3'} *}
     have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
     have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
     have invDeclC: "invDeclC 
@@ -934,8 +935,7 @@
       show ?thesis
 	by simp
     qed
-    from cls this
-    show ?case
+    with cls show ?case
       by (rule eval.Init)
   qed 
 qed
@@ -994,13 +994,14 @@
   show ?thesis .
 qed
 
+text {* *} (* FIXME *)
 
 lemma eval_evaln: 
- (assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
-          wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
-     conf_s0: "s0\<Colon>\<preceq>(G, L)" and
-          wf: "wf_prog G"  
- )  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
+  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
+            wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
+       conf_s0: "s0\<Colon>\<preceq>(G, L)" and
+            wf: "wf_prog G"  
+  shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
 proof -
   from eval 
   show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
@@ -1185,7 +1186,7 @@
 	with xcpt_s2 conf_s2 wf 
 	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
 	  by (auto dest: Try_lemma)
-	(* FIXME extract lemma for this conformance, also usefull for
+	(* FIXME extract lemma for this conformance, also useful for
                eval_type_sound and evaln_eval *)
 	from this wt_c2
 	obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -10,9 +10,9 @@
 section "error free"
  
 lemma error_free_halloc:
- (assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
+  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
           error_free_s0: "error_free s0"
- ) "error_free s1"
+  shows "error_free s1"
 proof -
   from halloc error_free_s0
   obtain abrupt0 store0 abrupt1 store1
@@ -37,8 +37,8 @@
 qed
 
 lemma error_free_sxalloc:
- (assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0") 
- "error_free s1"
+  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
+  shows "error_free s1"
 proof -
   from sxalloc error_free_s0
   obtain abrupt0 store0 abrupt1 store1
@@ -857,17 +857,17 @@
 
 (* #### stat raus und gleich is_static f schreiben *) 
 theorem dynamic_field_access_ok:
-  (assumes wf: "wf_prog G" and
-     not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
-    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
-    conform_s: "s\<Colon>\<preceq>(G, L)" and 
-     normal_s: "normal s" and
-         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
-            f: "accfield G accC statC fn = Some f" and
-         dynC: "if stat then dynC=declclass f  
-                        else dynC=obj_class (lookup_obj (store s) a)" and
-         stat: "if stat then (is_static f) else (\<not> is_static f)"
-  ) "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
+  assumes wf: "wf_prog G" and
+    not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
+   conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
+   conform_s: "s\<Colon>\<preceq>(G, L)" and 
+    normal_s: "normal s" and
+        wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
+           f: "accfield G accC statC fn = Some f" and
+        dynC: "if stat then dynC=declclass f  
+                       else dynC=obj_class (lookup_obj (store s) a)" and
+        stat: "if stat then (is_static f) else (\<not> is_static f)"
+  shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
      G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
 proof (cases "stat")
   case True
@@ -1017,7 +1017,7 @@
 *)
 
 lemma error_free_field_access:
- (assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
+  assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
               wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
          eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
             eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
@@ -1025,7 +1025,7 @@
             conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
               fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
                 wf: "wf_prog G"   
- ) "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
+  shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
 proof -
   from fvar
   have store_s2': "store s2'=store s2"
@@ -1066,12 +1066,12 @@
 qed
 
 lemma call_access_ok:
-(assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
-     and        wf: "wf_prog G" 
-     and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
-     and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
-     and      invC: "invC = invocation_class (invmode statM e) s a statT"
-)"\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
+  assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
+      and        wf: "wf_prog G" 
+      and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
+      and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
+      and      invC: "invC = invocation_class (invmode statM e) s a statT"
+  shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
   G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
 proof -
   from wt_e wf have type_statT: "is_type G (RefT statT)"
@@ -1123,7 +1123,7 @@
 qed
 
 lemma error_free_call_access:
- (assumes     
+  assumes
    eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
        statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
@@ -1138,7 +1138,7 @@
     invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
                              a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
           wf: "wf_prog G"
- )"check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
+  shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
    = s3"
 proof (cases "normal s2")
   case False
@@ -1198,11 +1198,11 @@
 section "main proof of type safety"
 
 lemma eval_type_sound:
-      (assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
-                 wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
-                 wf: "wf_prog G" and 
-            conf_s0: "s0\<Colon>\<preceq>(G,L)"           
-      ) "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
+  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
+            wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
+            wf: "wf_prog G" and 
+       conf_s0: "s0\<Colon>\<preceq>(G,L)"           
+  shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
          (error_free s0 = error_free s1)"
 proof -
   from eval 
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/WellForm.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -718,7 +718,8 @@
 qed
 
 lemma wf_prog_hidesD:
- (assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G") 
+  assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G"
+  shows
    "accmodi old \<le> accmodi new \<and>
     is_static old"
 proof -
@@ -759,7 +760,8 @@
 @{text wf_prog_dyn_override_prop}.
 *}
 lemma wf_prog_stat_overridesD:
- (assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G") 
+  assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G"
+  shows
    "G\<turnstile>resTy new\<preceq>resTy old \<and>
     accmodi old \<le> accmodi new \<and>
     \<not> is_static old"
@@ -790,8 +792,8 @@
 qed
     
 lemma static_to_dynamic_overriding: 
-  (assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G")
-   "G\<turnstile>new overrides old"
+  assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G"
+  shows "G\<turnstile>new overrides old"
 proof -
   from stat_override 
   show ?thesis (is "?Overrides new old")
@@ -827,14 +829,14 @@
 qed
 
 lemma non_Package_instance_method_inheritance:
-(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
-             accmodi_old: "accmodi old \<noteq> Package" and 
-         instance_method: "\<not> is_static old" and
-                  subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
-            old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
-                      wf: "wf_prog G"
-) "G\<turnstile>Method old member_of C \<or>
-   (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and>  G\<turnstile>Method new member_of C)"
+  assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
+              accmodi_old: "accmodi old \<noteq> Package" and 
+          instance_method: "\<not> is_static old" and
+                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
+             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
+                       wf: "wf_prog G"
+  shows "G\<turnstile>Method old member_of C \<or>
+   (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)"
 proof -
   from wf have ws: "ws_prog G" by auto
   from old_declared have iscls_declC_old: "is_class G (declclass old)"
@@ -989,17 +991,17 @@
 
 lemma non_Package_instance_method_inheritance_cases [consumes 6,
          case_names Inheritance Overriding]:
-(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
-             accmodi_old: "accmodi old \<noteq> Package" and 
-         instance_method: "\<not> is_static old" and
-                  subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
-            old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
-                      wf: "wf_prog G" and
-             inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
-             overriding:  "\<And> new. 
+  assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
+              accmodi_old: "accmodi old \<noteq> Package" and 
+          instance_method: "\<not> is_static old" and
+                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
+             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
+                       wf: "wf_prog G" and
+              inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
+               overriding: "\<And> new.
                            \<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
                            \<Longrightarrow> P"
-) "P"
+  shows P
 proof -
   from old_inheritable accmodi_old instance_method subcls old_declared wf 
        inheritance overriding
@@ -1008,10 +1010,10 @@
 qed
 
 lemma dynamic_to_static_overriding:
-(assumes dyn_override: "G\<turnstile> new overrides old" and
-          accmodi_old: "accmodi old \<noteq> Package" and
-                   wf: "wf_prog G"
-) "G\<turnstile> new overrides\<^sub>S old"  
+  assumes dyn_override: "G\<turnstile> new overrides old" and
+           accmodi_old: "accmodi old \<noteq> Package" and
+                    wf: "wf_prog G"
+  shows "G\<turnstile> new overrides\<^sub>S old"  
 proof - 
   from dyn_override accmodi_old
   show ?thesis (is "?Overrides new old")
@@ -1101,9 +1103,9 @@
 qed
 
 lemma wf_prog_dyn_override_prop:
- (assumes dyn_override: "G \<turnstile> new overrides old" and
+  assumes dyn_override: "G \<turnstile> new overrides old" and
                     wf: "wf_prog G"
- ) "accmodi old \<le> accmodi new"
+  shows "accmodi old \<le> accmodi new"
 proof (cases "accmodi old = Package")
   case True
   note old_Package = this
@@ -1130,10 +1132,10 @@
 qed 
 
 lemma overrides_Package_old: 
-(assumes dyn_override: "G \<turnstile> new overrides old" and 
-          accmodi_new: "accmodi new = Package" and
-                   wf: "wf_prog G "
-) "accmodi old = Package"
+  assumes dyn_override: "G \<turnstile> new overrides old" and 
+           accmodi_new: "accmodi new = Package" and
+                    wf: "wf_prog G "
+  shows "accmodi old = Package"
 proof (cases "accmodi old")
   case Private
   with dyn_override show ?thesis
@@ -1166,11 +1168,11 @@
 qed
 
 lemma dyn_override_Package:
- (assumes dyn_override: "G \<turnstile> new overrides old" and
-          accmodi_old: "accmodi old = Package" and 
-          accmodi_new: "accmodi new = Package" and
+  assumes dyn_override: "G \<turnstile> new overrides old" and
+           accmodi_old: "accmodi old = Package" and 
+           accmodi_new: "accmodi new = Package" and
                     wf: "wf_prog G"
- ) "pid (declclass old) = pid (declclass new)"
+  shows "pid (declclass old) = pid (declclass new)"
 proof - 
   from dyn_override accmodi_old accmodi_new
   show ?thesis (is "?EqPid old new")
@@ -1195,11 +1197,11 @@
 qed
 
 lemma dyn_override_Package_escape:
- (assumes dyn_override: "G \<turnstile> new overrides old" and
-          accmodi_old: "accmodi old = Package" and 
-         outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
+  assumes dyn_override: "G \<turnstile> new overrides old" and
+           accmodi_old: "accmodi old = Package" and 
+          outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
                     wf: "wf_prog G"
- ) "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
+  shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
              pid (declclass old) = pid (declclass inter) \<and>
              Protected \<le> accmodi inter"
 proof -
@@ -1373,10 +1375,11 @@
 qed
 
 lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
-(assumes methd_C: "methd G C sig = Some m" and
-                    ws: "ws_prog G" and
-                  clsC: "class G C = Some c" and
-             neq_C_Obj: "C\<noteq>Object" )  
+  assumes methd_C: "methd G C sig = Some m" and
+               ws: "ws_prog G" and
+             clsC: "class G C = Some c" and
+        neq_C_Obj: "C\<noteq>Object"
+  shows
 "\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
   \<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P 
  \<rbrakk> \<Longrightarrow> P"
@@ -1406,8 +1409,9 @@
 
   
 lemma methd_member_of:
- (assumes wf: "wf_prog G") 
-  "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
+  assumes wf: "wf_prog G"
+  shows
+    "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
   (is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 
 proof -
   from wf   have   ws: "ws_prog G" ..
@@ -1452,13 +1456,13 @@
             intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
 
 lemma wf_prog_staticD:
- (assumes     wf: "wf_prog G" and 
+  assumes     wf: "wf_prog G" and
             clsC: "class G C = Some c" and
        neq_C_Obj: "C \<noteq> Object" and 
              old: "methd G (super c) sig = Some old" and 
      accmodi_old: "Protected \<le> accmodi old" and
              new: "table_of (methods c) sig = Some new"
- ) "is_static new = is_static old"
+  shows "is_static new = is_static old"
 proof -
   from clsC wf 
   have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
@@ -1508,13 +1512,13 @@
 qed
 
 lemma inheritable_instance_methd: 
- (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
+  assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
               is_cls_D: "is_class G D" and
                     wf: "wf_prog G" and 
                    old: "methd G D sig = Some old" and
            accmodi_old: "Protected \<le> accmodi old" and  
         not_static_old: "\<not> is_static old"
- )  
+  shows
   "\<exists>new. methd G C sig = Some new \<and>
          (new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)"
  (is "(\<exists>new. (?Constraint C new old))")
@@ -1644,7 +1648,7 @@
 
 lemma inheritable_instance_methd_cases [consumes 6
                                        , case_names Inheritance Overriding]: 
- (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
+  assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
               is_cls_D: "is_class G D" and
                     wf: "wf_prog G" and 
                    old: "methd G D sig = Some old" and
@@ -1654,7 +1658,7 @@
             overriding:  "\<And> new. \<lbrakk>methd G C sig = Some new;
                                    G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
         
- ) "P"
+  shows P
 proof -
 from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
 show ?thesis
@@ -1662,13 +1666,13 @@
 qed
 
 lemma inheritable_instance_methd_props: 
- (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
+  assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
               is_cls_D: "is_class G D" and
                     wf: "wf_prog G" and 
                    old: "methd G D sig = Some old" and
            accmodi_old: "Protected \<le> accmodi old" and  
         not_static_old: "\<not> is_static old"
- )  
+  shows
   "\<exists>new. methd G C sig = Some new \<and>
           \<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new"
  (is "(\<exists>new. (?Constraint C new old))")
@@ -1976,11 +1980,11 @@
 *)
 
 lemma dynmethd_Object:
- (assumes statM: "methd G Object sig = Some statM" and
+  assumes statM: "methd G Object sig = Some statM" and
         private: "accmodi statM = Private" and 
        is_cls_C: "is_class G C" and
              wf: "wf_prog G"
- ) "dynmethd G Object C sig = Some statM"
+  shows "dynmethd G Object C sig = Some statM"
 proof -
   from is_cls_C wf 
   have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" 
@@ -2002,12 +2006,12 @@
 qed
 
 lemma wf_imethds_hiding_objmethdsD: 
-  (assumes     old: "methd G Object sig = Some old" and
-           is_if_I: "is_iface G I" and
-                wf: "wf_prog G" and    
-       not_private: "accmodi old \<noteq> Private" and
-               new: "new \<in> imethds G I sig" 
-  ) "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
+  assumes     old: "methd G Object sig = Some old" and
+          is_if_I: "is_iface G I" and
+               wf: "wf_prog G" and    
+      not_private: "accmodi old \<noteq> Private" and
+              new: "new \<in> imethds G I sig" 
+  shows "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
 proof -
   from wf have ws: "ws_prog G" by simp
   {
@@ -2102,10 +2106,10 @@
 "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
 
 lemma valid_lookup_cls_is_class:
- (assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
+  assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
       ty_statT: "isrtype G statT" and
             wf: "wf_prog G"
- ) "is_class G dynC"
+  shows "is_class G dynC"
 proof (cases statT)
   case NullT
   with dynC ty_statT show ?thesis
@@ -2503,10 +2507,10 @@
                  static_to_dynamic_overriding)
 
 lemma static_to_dynamic_accessible_from:
- (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
+  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
                 wf: "wf_prog G"
- ) "G\<turnstile>m in dynC dyn_accessible_from accC"
+  shows "G\<turnstile>m in dynC dyn_accessible_from accC"
 proof - 
   from stat_acc subclseq 
   show ?thesis (is "?Dyn_accessible m")
@@ -2528,10 +2532,10 @@
 qed
 
 lemma static_to_dynamic_accessible_from_static:
- (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
+  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
             static: "is_static m" and
                 wf: "wf_prog G"
- ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
+  shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
 proof -
   from stat_acc wf 
   have "G\<turnstile>m in statC dyn_accessible_from accC"
@@ -2542,10 +2546,10 @@
 qed
 
 lemma dynmethd_member_in:
- (assumes    m: "dynmethd G statC dynC sig = Some m" and
+  assumes    m: "dynmethd G statC dynC sig = Some m" and
    iscls_statC: "is_class G statC" and
             wf: "wf_prog G"
- ) "G\<turnstile>Methd sig m member_in dynC"
+  shows "G\<turnstile>Methd sig m member_in dynC"
 proof -
   from m 
   have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
@@ -2563,11 +2567,11 @@
 qed
 
 lemma dynmethd_access_prop:
-  (assumes statM: "methd G statC sig = Some statM" and
-        stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
-            dynM: "dynmethd G statC dynC sig = Some dynM" and
-              wf: "wf_prog G" 
-   ) "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
+  assumes statM: "methd G statC sig = Some statM" and
+       stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
+           dynM: "dynmethd G statC dynC sig = Some dynM" and
+             wf: "wf_prog G" 
+  shows "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
 proof -
   from wf have ws: "ws_prog G" ..
   from dynM 
@@ -2638,12 +2642,12 @@
 qed
 
 lemma implmt_methd_access:
-(fixes accC::qtname
- assumes iface_methd: "imethds G I sig \<noteq> {}" and
+  fixes accC::qtname
+  assumes iface_methd: "imethds G I sig \<noteq> {}" and
            implements: "G\<turnstile>dynC\<leadsto>I"  and
                isif_I: "is_iface G I" and
                    wf: "wf_prog G" 
- ) "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
+  shows "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
 proof -
   from implements 
@@ -2668,12 +2672,12 @@
 qed
 
 corollary implmt_dynimethd_access:
-(fixes accC::qtname
- assumes iface_methd: "imethds G I sig \<noteq> {}" and
+  fixes accC::qtname
+  assumes iface_methd: "imethds G I sig \<noteq> {}" and
            implements: "G\<turnstile>dynC\<leadsto>I"  and
                isif_I: "is_iface G I" and
                    wf: "wf_prog G" 
- ) "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
+  shows "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
 proof -
   from iface_methd
@@ -2686,12 +2690,12 @@
 qed
 
 lemma dynlookup_access_prop:
- (assumes emh: "emh \<in> mheads G accC statT sig" and
+  assumes emh: "emh \<in> mheads G accC statT sig" and
          dynM: "dynlookup G statT dynC sig = Some dynM" and
     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and
     isT_statT: "isrtype G statT" and
            wf: "wf_prog G"
- ) "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
+  shows "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
 proof -
   from emh wf
   have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)"
@@ -2835,11 +2839,11 @@
 qed
 
 lemma dynlookup_access:
- (assumes emh: "emh \<in> mheads G accC statT sig" and
+  assumes emh: "emh \<in> mheads G accC statT sig" and
     dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and
     isT_statT: "isrtype G statT" and
            wf: "wf_prog G"
- ) "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
+  shows "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
             G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
 proof - 
   from dynC_prop isT_statT wf
@@ -2855,10 +2859,10 @@
 qed
 
 lemma stat_overrides_Package_old: 
-(assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
+  assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
           accmodi_new: "accmodi new = Package" and
                    wf: "wf_prog G "
-) "accmodi old = Package"
+  shows "accmodi old = Package"
 proof -
   from stat_override wf 
   have "accmodi old \<le> accmodi new"
@@ -2916,12 +2920,12 @@
 since methods can break the package bounds due to overriding
 *}
 lemma dyn_accessible_instance_field_Protected:
- (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
+  assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
              prot: "accmodi f = Protected" and
             field: "is_field f" and
    instance_field: "\<not> is_static f" and
           outside: "pid (declclass f) \<noteq> pid accC"
- ) "G\<turnstile> C \<preceq>\<^sub>C accC"
+  shows "G\<turnstile> C \<preceq>\<^sub>C accC"
 proof -
   from dyn_acc prot field instance_field outside
   show ?thesis
@@ -2941,12 +2945,12 @@
 qed
    
 lemma dyn_accessible_static_field_Protected:
- (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
+  assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
              prot: "accmodi f = Protected" and
             field: "is_field f" and
      static_field: "is_static f" and
           outside: "pid (declclass f) \<noteq> pid accC"
- ) "G\<turnstile> accC \<preceq>\<^sub>C declclass f  \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
+  shows "G\<turnstile> accC \<preceq>\<^sub>C declclass f  \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
 proof -
   from dyn_acc prot field static_field outside
   show ?thesis
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -265,10 +265,10 @@
   apply simp
   done
 
-lemma finite_lessThan [iff]: (fixes k :: nat) "finite {..k(}"
+lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
   by (induct k) (simp_all add: lessThan_Suc)
 
-lemma finite_atMost [iff]: (fixes k :: nat) "finite {..k}"
+lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
   by (induct k) (simp_all add: atMost_Suc)
 
 lemma bounded_nat_set_is_finite:
@@ -814,10 +814,12 @@
     apply auto
   done
 
-lemma setsum_UN_disjoint: (fixes f :: "'a => 'b::plus_ac0")
-  "finite I ==> (ALL i:I. finite (A i)) ==>
-      (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
-    setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
+lemma setsum_UN_disjoint:
+  fixes f :: "'a => 'b::plus_ac0"
+  shows
+    "finite I ==> (ALL i:I. finite (A i)) ==>
+        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+      setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
   apply (induct set: Finites)
    apply simp
   apply atomize
@@ -939,7 +941,7 @@
   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
   done
 
-theorem n_subsets: "finite A ==> card {B. B <= A & card(B) = k} = (card A choose k)"
+theorem n_subsets: "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
   by (simp add: n_sub_lemma)
 
 end
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/HOL.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -201,7 +201,10 @@
 subsubsection {* Intuitionistic Reasoning *}
 
 lemma impE':
-  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
+  assumes 1: "P --> Q"
+    and 2: "Q ==> R"
+    and 3: "P --> Q ==> P"
+  shows R
 proof -
   from 3 and 1 have P .
   with 1 have Q by (rule impE)
@@ -209,13 +212,18 @@
 qed
 
 lemma allE':
-  (assumes 1: "ALL x. P x" and 2: "P x ==> ALL x. P x ==> Q") Q
+  assumes 1: "ALL x. P x"
+    and 2: "P x ==> ALL x. P x ==> Q"
+  shows Q
 proof -
   from 1 have "P x" by (rule spec)
   from this and 1 show Q by (rule 2)
 qed
 
-lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
+lemma notE':
+  assumes 1: "~ P"
+    and 2: "~ P ==> P"
+  shows R
 proof -
   from 2 and 1 have P .
   with 1 show R by (rule notE)
@@ -309,7 +317,8 @@
 lemma eta_contract_eq: "(%s. f s) = f" ..
 
 lemma simp_thms:
-  (not_not: "(~ ~ P) = P" and
+  shows not_not: "(~ ~ P) = P"
+  and
     "(P ~= Q) = (P = (~Q))"
     "(P | ~P) = True"    "(~P | P) = True"
     "((~P) = (~Q)) = (P=Q)"
@@ -333,7 +342,7 @@
     "!!P. (EX x. x=t & P(x)) = P(t)"
     "!!P. (EX x. t=x & P(x)) = P(t)"
     "!!P. (ALL x. x=t --> P(x)) = P(t)"
-    "!!P. (ALL x. t=x --> P(x)) = P(t)")
+    "!!P. (ALL x. t=x --> P(x)) = P(t)"
   by (blast, blast, blast, blast, blast, rules+)
  
 lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
@@ -360,19 +369,19 @@
   by (rules | blast)+
 
 lemma eq_ac:
- (eq_commute: "(a=b) = (b=a)" and
-  eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" and
-  eq_assoc: "((P=Q)=R) = (P=(Q=R))") by (rules, blast+)
+  shows eq_commute: "(a=b) = (b=a)"
+    and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
+    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
 lemma neq_commute: "(a~=b) = (b~=a)" by rules
 
 lemma conj_comms:
- (conj_commute: "(P&Q) = (Q&P)" and
-  conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by rules+
+  shows conj_commute: "(P&Q) = (Q&P)"
+    and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+
 lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
 
 lemma disj_comms:
- (disj_commute: "(P|Q) = (Q|P)" and
-  disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by rules+
+  shows disj_commute: "(P|Q) = (Q|P)"
+    and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by rules+
 lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
 
 lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Induct/Term.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -42,9 +42,9 @@
 text {* \medskip Alternative induction rule *}
 
 lemma
-  (assumes var: "!!v. P (Var v)"
-    and app: "!!f ts. list_all P ts ==> P (App f ts)")
-  term_induct2: "P t"
+  assumes var: "!!v. P (Var v)"
+    and app: "!!f ts. list_all P ts ==> P (App f ts)"
+  shows term_induct2: "P t"
 and "list_all P ts"
   apply (induct t and ts)
      apply (rule var)
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Set.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -212,7 +212,7 @@
 lemma CollectD: "a : {x. P(x)} ==> P(a)"
   by simp
 
-lemma set_ext: (assumes prem: "(!!x. (x:A) = (x:B))") "A = B"
+lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
   apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
    apply (rule Collect_mem_eq)
   apply (rule Collect_mem_eq)
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -58,9 +58,9 @@
   done
 
 theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
-  (assumes a: "(a, b) : r^*"
-    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
-  "P b"
+  assumes a: "(a, b) : r^*"
+    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z"
+  shows "P b"
 proof -
   from a have "a = a --> P b"
     by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
@@ -151,14 +151,16 @@
   done
 
 theorem rtrancl_converseD:
-  (assumes r: "(x, y) \<in> (r^-1)^*") "(y, x) \<in> r^*"
+  assumes r: "(x, y) \<in> (r^-1)^*"
+  shows "(y, x) \<in> r^*"
 proof -
   from r show ?thesis
     by induct (rules intro: rtrancl_trans dest!: converseD)+
 qed
 
 theorem rtrancl_converseI:
-  (assumes r: "(y, x) \<in> r^*") "(x, y) \<in> (r^-1)^*"
+  assumes r: "(y, x) \<in> r^*"
+  shows "(x, y) \<in> (r^-1)^*"
 proof -
   from r show ?thesis
     by induct (rules intro: rtrancl_trans converseI)+
@@ -168,9 +170,9 @@
   by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
 
 theorem converse_rtrancl_induct:
-  (assumes major: "(a, b) : r^*"
-   and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y")
-    "P a"
+  assumes major: "(a, b) : r^*"
+    and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
+  shows "P a"
 proof -
   from rtrancl_converseI [OF major]
   show ?thesis
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/ex/Locales.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -143,8 +143,8 @@
 *}
 
 theorem (in group_context)
-  (assumes eq: "e \<cdot> x = x")
-  one_equality: "\<one> = e"
+  assumes eq: "e \<cdot> x = x"
+  shows one_equality: "\<one> = e"
 proof -
   have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
   also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
@@ -155,8 +155,8 @@
 qed
 
 theorem (in group_context)
-  (assumes eq: "x' \<cdot> x = \<one>")
-  inv_equality: "x\<inv> = x'"
+  assumes eq: "x' \<cdot> x = \<one>"
+  shows inv_equality: "x\<inv> = x'"
 proof -
   have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
   also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
@@ -214,8 +214,8 @@
 qed
 
 theorem (in group_context)
-  (assumes eq: "x\<inv> = y\<inv>")
-  inv_inject: "x = y"
+  assumes eq: "x\<inv> = y\<inv>"
+  shows inv_inject: "x = y"
 proof -
   have "x = x \<cdot> \<one>" by (simp only: right_one)
   also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
@@ -335,8 +335,9 @@
   versions of the @{text group} locale above.
 *}
 
-lemma (uses group G + group H)
-  "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
+lemma
+  uses group G + group H
+  shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
   "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
   "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
 
diff -r 84eb6c75cfe3 -r 0c4fd7529467 src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Mon Feb 25 20:46:09 2002 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy	Mon Feb 25 20:48:14 2002 +0100
@@ -53,9 +53,11 @@
   apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases)
   done
 
-lemma (notes rews = tree_forest.con_defs tree_def forest_def)
-  tree_forest_unfold: "tree_forest(A) =
-    (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
+lemma
+  notes rews = tree_forest.con_defs tree_def forest_def
+  shows
+    tree_forest_unfold: "tree_forest(A) =
+      (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
     -- {* NOT useful, but interesting \dots *}
   apply (unfold tree_def forest_def)
   apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
@@ -169,9 +171,10 @@
   \medskip @{text map}.
 *}
 
-lemma (assumes h_type: "!!x. x \<in> A ==> h(x): B")
-    map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
-  and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
+lemma
+  assumes h_type: "!!x. x \<in> A ==> h(x): B"
+  shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
+    and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
   apply (induct rule: tree_forest.mutual_induct)
     apply (insert h_type)
     apply simp_all