# HG changeset patch
# User kleing
# Date 1015171148 -3600
# Node ID 51c5f3f11d1659b72fe56126ec3bb0799212dad7
# Parent  42a54d6cec15f4cf1b027da6ded1ad0e40c91454
symbolized

diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -276,8 +276,7 @@
   apply simp
   done
 
-text {* Some shorthands to make the welltyping of method @{term
-makelist_name} easier to read *} 
+text {* Some abbreviations for readability *} 
 syntax
   list :: ty 
   test :: ty
@@ -382,4 +381,4 @@
   apply (simp add: conf_def start_heap_def)
   done
 
-end
\ No newline at end of file
+end
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -17,42 +17,42 @@
 
 constdefs
   wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
-                exception_table,p_count] => bool"
+                exception_table,p_count] \<Rightarrow> bool"
   "wt_instr i G rT phi mxs max_pc et pc == 
   app i G mxs rT pc et (phi!pc) \<and>
   (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
 
-  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
+  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
   "wt_start G C pTs mxl phi == 
   G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
 
   wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
-                 exception_table,method_type] => bool"
+                 exception_table,method_type] \<Rightarrow> bool"
   "wt_method G C pTs rT mxs mxl ins et phi ==
   let max_pc = length ins in
   0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
-  (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
+  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
 
-  wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
+  wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
   "wt_jvm_prog G phi ==
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
            wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
 
 
 lemma wt_jvm_progD:
-  "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
+  "wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
   by (unfold wt_jvm_prog_def, blast)
 
 lemma wt_jvm_prog_impl_wt_instr:
-  "[| wt_jvm_prog G phi; is_class G C;
-      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins |] 
-  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
+  "\<lbrakk> wt_jvm_prog G phi; is_class G C;
+      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk> 
+  \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
   by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
       simp, simp, simp add: wf_mdecl_def wt_method_def)
 
 lemma wt_jvm_prog_impl_wt_start:
-  "[| wt_jvm_prog G phi; is_class G C;
-      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) |] ==> 
+  "\<lbrakk> wt_jvm_prog G phi; is_class G C;
+      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow> 
   0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
   by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
       simp, simp, simp add: wf_mdecl_def wt_method_def)
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -31,9 +31,9 @@
   can directly infer that the current instruction is well typed:
 *}
 lemma wt_jvm_prog_impl_wt_instr_cor:
-  "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
-      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
+  "\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
+      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+  \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
 apply (unfold correct_state_def Let_def correct_frame_def)
 apply simp
 apply (blast intro: wt_jvm_prog_impl_wt_instr)
@@ -57,10 +57,10 @@
   @{text match_exception_table} from the operational semantics:
 *}
 lemma in_match_any:
-  "match_exception_table G xcpt pc et = Some pc' ==> 
+  "match_exception_table G xcpt pc et = Some pc' \<Longrightarrow> 
   \<exists>C. C \<in> set (match_any G pc et) \<and> G \<turnstile> xcpt \<preceq>C C \<and> 
       match_exception_table G C pc et = Some pc'"
-  (is "PROP ?P et" is "?match et ==> ?match_any et")
+  (is "PROP ?P et" is "?match et \<Longrightarrow> ?match_any et")
 proof (induct et)  
   show "PROP ?P []" 
     by simp
@@ -131,10 +131,10 @@
   conforms. 
 *}
 lemma uncaught_xcpt_correct:
-  "!!f. [| wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
-      G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> |]
-  ==> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>" 
-  (is "!!f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) |] ==> ?correct (?find frs)")
+  "\<And>f. \<lbrakk> wt_jvm_prog G phi; xcp = Addr adr; hp adr = Some T;
+      G,phi \<turnstile>JVM (None, hp, f#frs)\<surd> \<rbrakk>
+  \<Longrightarrow> G,phi \<turnstile>JVM (find_handler G (Some xcp) hp frs)\<surd>" 
+  (is "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs) \<rbrakk> \<Longrightarrow> ?correct (?find frs)")
 proof (induct frs) 
   -- "the base case is trivial, as it should be"
   show "?correct (?find [])" by (simp add: correct_state_def)
@@ -153,9 +153,9 @@
 
   -- "the induction hypothesis as produced by Isabelle, immediatly simplified
     with the fixed assumptions above"
-  assume "\<And>f. [| ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') |] ==> ?correct (?find frs')"  
+  assume "\<And>f. \<lbrakk> ?wt; ?adr; ?hp; ?correct (None, hp, f#frs') \<rbrakk> \<Longrightarrow> ?correct (?find frs')"  
   with wt adr hp 
-  have IH: "\<And>f. ?correct (None, hp, f#frs') ==> ?correct (?find frs')" by blast
+  have IH: "\<And>f. ?correct (None, hp, f#frs') \<Longrightarrow> ?correct (?find frs')" by blast
 
   from cr
   have cr': "?correct (None, hp, f'#frs')" by (auto simp add: correct_state_def)
@@ -249,11 +249,11 @@
   for welltyped instructions and conformant states:
 *}
 lemma exec_instr_xcpt_hp:
-  "[|  fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
+  "\<lbrakk>  fst (exec_instr (ins!pc) G hp stk vars Cl sig pc frs) = Some xcp;
        wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
-       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-  ==> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" 
-  (is "[| ?xcpt; ?wt; ?correct |] ==> ?thesis")
+       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+  \<Longrightarrow> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" 
+  (is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> ?thesis")
 proof -
   note [simp] = split_beta raise_system_xcpt_def
   note [split] = split_if_asm option.split_asm 
@@ -279,13 +279,13 @@
   resulting next state always conforms:
 *}
 lemma xcpt_correct:
-  "[| wt_jvm_prog G phi;
+  "\<lbrakk> wt_jvm_prog G phi;
       method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
       wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
       fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = Some xcp; 
       Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-  ==> G,phi \<turnstile>JVM state'\<surd>"
+      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+  \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 proof -
   assume wtp: "wt_jvm_prog G phi"
   assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -588,47 +588,47 @@
 lemmas [iff] = not_Err_eq
 
 lemma Load_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
     method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
     ins!pc = Load idx; 
     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (blast intro: approx_loc_imp_approx_val_sup)
 done
 
 lemma Store_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
   ins!pc = Store idx;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc;
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (blast intro: approx_loc_subst)
 done
 
 
 lemma LitPush_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
     method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
     ins!pc = LitPush v;
     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
-    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>" 
+    G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
 apply (clarsimp simp add: defs1 sup_PTS_eq map_eq_Cons)
 apply (blast dest: conf_litval intro: conf_widen)
 done
 
 
 lemma Cast_conf2:
-  "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
-      G\<turnstile>Class C\<preceq>T; is_class G C|] 
-  ==> G,h\<turnstile>v::\<preceq>T"
+  "\<lbrakk> wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; 
+      G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
+  \<Longrightarrow> G,h\<turnstile>v::\<preceq>T"
 apply (unfold cast_ok_def)
 apply (frule widen_Class)
 apply (elim exE disjE) 
@@ -641,28 +641,28 @@
 lemmas defs1 = defs1 raise_system_xcpt_def
 
 lemma Checkcast_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
     method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
     ins!pc = Checkcast D; 
     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
     Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
     G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
-    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+    fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 wt_jvm_prog_def map_eq_Cons split: split_if_asm)
 apply (blast intro: Cast_conf2)
 done
 
 
 lemma Getfield_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins!pc = Getfield F D; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
-  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons wt_jvm_prog_def 
                 split: option.split split_if_asm)
 apply (frule conf_widen)
@@ -687,14 +687,14 @@
 
 
 lemma Putfield_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins!pc = Putfield F D; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
-  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 split_beta split: option.split List.split split_if_asm)
 apply (frule conf_widen)
 prefer 2
@@ -715,14 +715,14 @@
     
 
 lemma New_correct:
-"[| wf_prog wt G;
+"\<lbrakk> wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins!pc = New X; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
-  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 proof -
   assume wf:   "wf_prog wt G"
   assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -793,14 +793,14 @@
 
 
 lemma Invoke_correct: 
-"[| wt_jvm_prog G phi; 
+"\<lbrakk> wt_jvm_prog G phi; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Invoke C' mn pTs; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
-  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
-==> G,phi \<turnstile>JVM state'\<surd>" 
+  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
 proof -
   assume wtprog: "wt_jvm_prog G phi"
   assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -972,13 +972,13 @@
 lemmas [simp del] = map_append
 
 lemma Return_correct:
-"[| wt_jvm_prog G phi; 
+"\<lbrakk> wt_jvm_prog G phi; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Return; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 proof -
   assume wt_prog: "wt_jvm_prog G phi"
   assume meth: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
@@ -1098,110 +1098,110 @@
 lemmas [simp] = map_append
 
 lemma Goto_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Goto branch; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
 apply fast
 done
 
 
 lemma Ifcmpeq_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Ifcmpeq branch; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
 apply fast
 done
 
 lemma Pop_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Pop;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
 apply fast
 done
 
 lemma Dup_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Dup;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
 lemma Dup_x1_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Dup_x1;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
 lemma Dup_x2_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Dup_x2;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
 lemma Swap_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Swap;
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (blast intro: conf_widen)
 done
 
 lemma IAdd_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = IAdd; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
 apply blast
 done
 
 lemma Throw_correct:
-"[| wf_prog wt G; 
+"\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); 
   ins ! pc = Throw; 
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
-  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
   by simp
 
 
@@ -1213,11 +1213,11 @@
   into another conforming state when one instruction is executed.
 *}
 theorem instr_correct:
-"[| wt_jvm_prog G phi;
+"\<lbrakk> wt_jvm_prog G phi;
   method (G,C) sig = Some (C,rT,maxs,maxl,ins,et);
   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
-  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
-==> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (frule wt_jvm_prog_impl_wt_instr_cor)
 apply assumption+
 apply (cases "fst (exec_instr (ins!pc) G hp stk loc C sig pc frs)")
@@ -1254,13 +1254,13 @@
 
 lemma correct_state_impl_Some_method:
   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
-  ==> \<exists>meth. method (G,C) sig = Some(C,meth)"
+  \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
 by (auto simp add: correct_state_def Let_def)
 
 
 lemma BV_correct_1 [rule_format]:
-"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] 
- ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>"
+"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
+ \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (simp only: split_tupled_all)
 apply (rename_tac xp hp frs)
 apply (case_tac xp)
@@ -1277,19 +1277,19 @@
 
 
 lemma L0:
-  "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
+  "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
 by (clarsimp simp add: neq_Nil_conv split_beta)
 
 lemma L1:
-  "[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|] 
-  ==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
+  "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
+  \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
 apply (drule L0)
 apply assumption
 apply (fast intro: BV_correct_1)
 done
 
 theorem BV_correct [rule_format]:
-"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
+"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
 apply (unfold exec_all_def)
 apply (erule rtrancl_induct)
  apply simp
@@ -1297,9 +1297,9 @@
 done
 
 theorem BV_correct_implies_approx:
-"[| wt_jvm_prog G phi; 
-    G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] 
-==> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and> 
+"\<lbrakk> wt_jvm_prog G phi; 
+    G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
+\<Longrightarrow> approx_stk G hp stk (fst (the (phi C sig ! pc))) \<and> 
     approx_loc G hp loc (snd (the (phi C sig ! pc)))"
 apply (drule BV_correct)
 apply assumption+
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -12,23 +12,23 @@
 theory Correct = BVSpec + JVMExec:
 
 constdefs
-  approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
-  "approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T"
+  approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
+  "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T"
 
-  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
+  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
   "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
 
-  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
+  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
   "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
 
-  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
+  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
   "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
                          approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
                          pc < length ins \<and> length loc=length(snd sig)+maxl+1"
 
 
 consts
- correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"
+ correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
 primrec
 "correct_frames G hp phi rT0 sig0 [] = True"
 
@@ -50,13 +50,13 @@
 
 
 constdefs
- correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
+ correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
                   ("_,_ |-JVM _ [ok]"  [51,51] 50)
 "correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
-     None => (case frs of
-             [] => True
-             | (f#fs) => G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 
+     None \<Rightarrow> (case frs of
+             [] \<Rightarrow> True
+             | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 
       (let (stk,loc,C,sig,pc) = f
              in
                          \<exists>rT maxs maxl ins et s.
@@ -65,11 +65,11 @@
                          phi C sig ! pc = Some s \<and>
        correct_frame G hp s maxl ins f \<and> 
              correct_frames G hp phi rT sig fs))
-   | Some x => frs = []" 
+   | Some x \<Rightarrow> frs = []" 
 
 
 syntax (xsymbols)
- correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
+ correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
                   ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
 
 
@@ -99,8 +99,8 @@
   by (cases T) (blast intro: conf_hext)+
 
 lemma approx_val_heap_update:
-  "[| hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] 
-  ==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
+  "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
+  \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
   by (cases v, auto simp add: obj_ty_def conf_def)
 
 lemma approx_val_widen:
@@ -228,8 +228,8 @@
 section {* oconf *}
 
 lemma oconf_field_update:
-  "[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |]
-  ==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
+  "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
+  \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
   by (simp add: oconf_def lconf_def)
 
 lemma oconf_newref:
@@ -290,11 +290,11 @@
 
 lemma correct_frames_field_update [rule_format]:
   "\<forall>rT C sig. 
-  correct_frames G hp phi rT sig frs --> 
-  hp a = Some (C,fs) --> 
-  map_of (fields (G, C)) fl = Some fd --> 
+  correct_frames G hp phi rT sig frs \<longrightarrow> 
+  hp a = Some (C,fs) \<longrightarrow> 
+  map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
   G,hp\<turnstile>v::\<preceq>fd 
-  --> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
+  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
 apply (induct frs)
  apply simp
 apply clarify
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -13,7 +13,7 @@
 
 text {* Program counter of successor instructions: *}
 consts
-  succs :: "instr => p_count => p_count list"
+  succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"
 primrec 
   "succs (Load idx) pc         = [pc+1]"
   "succs (Store idx) pc        = [pc+1]"
@@ -36,7 +36,7 @@
 
 text "Effect of instruction on the state type:"
 consts 
-eff' :: "instr \<times> jvm_prog \<times> state_type => state_type"
+eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
 
 recdef eff' "{}"
 "eff' (Load idx,  G, (ST, LT))          = (ok_val (LT ! idx) # ST, LT)"
@@ -84,7 +84,7 @@
   by (induct et) auto
 
 consts
-  xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table => cname list" 
+  xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table \<Rightarrow> cname list" 
 recdef xcpt_names "{}"
   "xcpt_names (Getfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et" 
   "xcpt_names (Putfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et" 
@@ -104,7 +104,7 @@
   norm_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
   "norm_eff i G == option_map (\<lambda>s. eff' (i,G,s))"
 
-  eff :: "instr => jvm_prog => p_count => exception_table => state_type option => succ_type"
+  eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> succ_type"
   "eff i G pc et s == (map (\<lambda>pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"
 
 constdefs
@@ -127,7 +127,7 @@
 
 text "Conditions under which eff is applicable:"
 consts
-app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type => bool"
+app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type \<Rightarrow> bool"
 
 recdef app' "{}"
 "app' (Load idx, G, pc, maxs, rT, s) = 
@@ -180,17 +180,17 @@
   xcpt_app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> bool"
   "xcpt_app i G pc et \<equiv> \<forall>C\<in>set(xcpt_names (i,G,pc,et)). is_class G C"
 
-  app :: "instr => jvm_prog => nat => ty => nat => exception_table => state_type option => bool"
-  "app i G maxs rT pc et s == case s of None => True | Some t => app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"
+  app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> exception_table \<Rightarrow> state_type option \<Rightarrow> bool"
+  "app i G maxs rT pc et s == case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,pc,maxs,rT,t) \<and> xcpt_app i G pc et"
 
 
-lemma 1: "2 < length a ==> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
+lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
 proof (cases a)
   fix x xs assume "a = x#xs" "2 < length a"
   thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
 qed auto
 
-lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
+lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
 proof -;
   assume "\<not>(2 < length a)"
   hence "length a < (Suc (Suc (Suc 0)))" by simp
@@ -203,7 +203,7 @@
     hence "\<exists> l. x = [l]"  by - (cases x, auto)
   } note 0 = this
 
-  have "length a = Suc (Suc 0) ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+  have "length a = Suc (Suc 0) \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
   with * show ?thesis by (auto dest: 0)
 qed
 
@@ -337,7 +337,7 @@
 proof (cases (open) s)
   note list_all2_def [simp]
   case Pair
-  have "?app (a,b) ==> ?P (a,b)"
+  have "?app (a,b) \<Longrightarrow> ?P (a,b)"
   proof -
     assume app: "?app (a,b)"
     hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> 
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -14,7 +14,7 @@
 
 
 lemma sup_loc_some [rule_format]:
-"\<forall>y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t --> 
+"\<forall>y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = OK t \<longrightarrow> 
   (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
 proof (induct (open) ?P b)
   show "?P []" by simp
@@ -41,9 +41,9 @@
    
 
 lemma all_widen_is_sup_loc:
-"\<forall>b. length a = length b --> 
+"\<forall>b. length a = length b \<longrightarrow> 
      (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))" 
- (is "\<forall>b. length a = length b --> ?Q a b" is "?P a")
+ (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
 proof (induct "a")
   show "?P []" by simp
 
@@ -60,7 +60,7 @@
  
 
 lemma append_length_n [rule_format]: 
-"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
+"\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
 proof (induct (open) ?P x)
   show "?P []" by simp
 
@@ -86,7 +86,7 @@
 qed
 
 lemma rev_append_cons:
-"n < length x ==> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
+"n < length x \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
 proof -
   assume n: "n < length x"
   hence "n \<le> length x" by simp
@@ -109,7 +109,7 @@
 lemmas [iff] = not_Err_eq
 
 lemma app_mono: 
-"[|G \<turnstile> s <=' s'; app i G m rT pc et s'|] ==> app i G m rT pc et s"
+"\<lbrakk>G \<turnstile> s <=' s'; app i G m rT pc et s'\<rbrakk> \<Longrightarrow> app i G m rT pc et s"
 proof -
 
   { fix s1 s2
@@ -281,7 +281,7 @@
 lemmas [simp del] = split_paired_Ex
 
 lemma eff'_mono:
-"[| app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 |] ==>
+"\<lbrakk> app i G m rT pc et (Some s2); G \<turnstile> s1 <=s s2 \<rbrakk> \<Longrightarrow>
   G \<turnstile> eff' (i,G,s1) <=s eff' (i,G,s2)"
 proof (cases s1, cases s2)
   fix a1 b1 a2 b2
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -12,48 +12,48 @@
 
 datatype 'a err = Err | OK 'a
 
-types 'a ebinop = "'a => 'a => 'a err"
+types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
       'a esl =    "'a set * 'a ord * 'a ebinop"
 
 consts
-  ok_val :: "'a err => 'a"
+  ok_val :: "'a err \<Rightarrow> 'a"
 primrec
   "ok_val (OK x) = x"
 
 constdefs
- lift :: "('a => 'b err) => ('a err => 'b err)"
-"lift f e == case e of Err => Err | OK x => f x"
+ lift :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+"lift f e == case e of Err \<Rightarrow> Err | OK x \<Rightarrow> f x"
 
- lift2 :: "('a => 'b => 'c err) => 'a err => 'b err => 'c err"
+ lift2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a err \<Rightarrow> 'b err \<Rightarrow> 'c err"
 "lift2 f e1 e2 ==
- case e1 of Err  => Err
-          | OK x => (case e2 of Err => Err | OK y => f x y)"
+ case e1 of Err  \<Rightarrow> Err
+          | OK x \<Rightarrow> (case e2 of Err \<Rightarrow> Err | OK y \<Rightarrow> f x y)"
 
- le :: "'a ord => 'a err ord"
+ le :: "'a ord \<Rightarrow> 'a err ord"
 "le r e1 e2 ==
-        case e2 of Err => True |
-                   OK y => (case e1 of Err => False | OK x => x <=_r y)"
+        case e2 of Err \<Rightarrow> True |
+                   OK y \<Rightarrow> (case e1 of Err \<Rightarrow> False | OK x \<Rightarrow> x <=_r y)"
 
- sup :: "('a => 'b => 'c) => ('a err => 'b err => 'c err)"
+ sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> 'c err)"
 "sup f == lift2(%x y. OK(x +_f y))"
 
- err :: "'a set => 'a err set"
+ err :: "'a set \<Rightarrow> 'a err set"
 "err A == insert Err {x . ? y:A. x = OK y}"
 
- esl :: "'a sl => 'a esl"
+ esl :: "'a sl \<Rightarrow> 'a esl"
 "esl == %(A,r,f). (A,r, %x y. OK(f x y))"
 
- sl :: "'a esl => 'a err sl"
+ sl :: "'a esl \<Rightarrow> 'a err sl"
 "sl == %(A,r,f). (err A, le r, lift2 f)"
 
 syntax
- err_semilat :: "'a esl => bool"
+ err_semilat :: "'a esl \<Rightarrow> bool"
 translations
 "err_semilat L" == "semilat(Err.sl L)"
 
 
 consts
-  strict  :: "('a => 'b err) => ('a err => 'b err)"
+  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
 primrec
   "strict f Err    = Err"
   "strict f (OK x) = f x"
@@ -75,20 +75,20 @@
   by (simp add: lesub_def)
 
 lemma le_err_refl:
-  "!x. x <=_r x ==> e <=_(Err.le r) e"
+  "!x. x <=_r x \<Longrightarrow> e <=_(Err.le r) e"
 apply (unfold lesub_def Err.le_def)
 apply (simp split: err.split)
 done 
 
 lemma le_err_trans [rule_format]:
-  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"
+  "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e3 \<longrightarrow> e1 <=_(le r) e3"
 apply (unfold unfold_lesub_err le_def)
 apply (simp split: err.split)
 apply (blast intro: order_trans)
 done
 
 lemma le_err_antisym [rule_format]:
-  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"
+  "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e1 \<longrightarrow> e1=e2"
 apply (unfold unfold_lesub_err le_def)
 apply (simp split: err.split)
 apply (blast intro: order_antisym)
@@ -136,20 +136,20 @@
   by (simp add: lesssub_def lesub_def le_def split: err.split)
 
 lemma semilat_errI:
-  "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+  "semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
 apply (unfold semilat_Def closed_def plussub_def lesub_def 
               lift2_def Err.le_def err_def)
 apply (simp split: err.split)
 done
 
 lemma err_semilat_eslI: 
-  "!!L. semilat L ==> err_semilat(esl L)"
+  "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
 apply (unfold sl_def esl_def)
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply (simp add: semilat_errI)
 done
 
-lemma acc_err [simp, intro!]:  "acc r ==> acc(le r)"
+lemma acc_err [simp, intro!]:  "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
 apply (simp add: wf_eq_minimal split: err.split)
 apply clarify
@@ -170,7 +170,7 @@
 section {* lift *}
 
 lemma lift_in_errI:
-  "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
+  "\<lbrakk> e : err S; !x:S. e = OK x \<longrightarrow> f x : err S \<rbrakk> \<Longrightarrow> lift f e : err S"
 apply (unfold lift_def)
 apply (simp split: err.split)
 apply blast
@@ -221,42 +221,42 @@
 section {* semilat (err A) (le r) f *}
 
 lemma semilat_le_err_Err_plus [simp]:
-  "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
+  "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
   by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
 
 lemma semilat_le_err_plus_Err [simp]:
-  "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"
+  "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
   by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
 
 lemma semilat_le_err_OK1:
-  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
-  ==> x <=_r z";
+  "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
+  \<Longrightarrow> x <=_r z";
 apply (rule OK_le_err_OK [THEN iffD1])
 apply (erule subst)
 apply simp
 done 
 
 lemma semilat_le_err_OK2:
-  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
-  ==> y <=_r z"
+  "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
+  \<Longrightarrow> y <=_r z"
 apply (rule OK_le_err_OK [THEN iffD1])
 apply (erule subst)
 apply simp
 done 
 
 lemma eq_order_le:
-  "[| x=y; order r |] ==> x <=_r y"
+  "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
 apply (unfold order_def)
 apply blast
 done
 
 lemma OK_plus_OK_eq_Err_conv [simp]:
-  "[| x:A; y:A; semilat(err A, le r, fe) |] ==> 
+  "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow> 
   ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
 proof -
-  have plus_le_conv3: "!!A x y z f r. 
-    [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
-    ==> x <=_r z \<and> y <=_r z"
+  have plus_le_conv3: "\<And>A x y z f r. 
+    \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> 
+    \<Longrightarrow> x <=_r z \<and> y <=_r z"
     by (rule plus_le_conv [THEN iffD1])
   case rule_context
   thus ?thesis
@@ -287,13 +287,13 @@
 
 (* FIXME? *)
 lemma all_bex_swap_lemma [iff]:
-  "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"
+  "(!x. (? y:A. x = f y) \<longrightarrow> P x) = (!y:A. P(f y))"
   by blast
 
 lemma closed_err_Union_lift2I: 
-  "[| !A:AS. closed (err A) (lift2 f); AS ~= {}; 
-      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] 
-  ==> closed (err(Union AS)) (lift2 f)"
+  "\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {}; 
+      !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk> 
+  \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
 apply (unfold closed_def err_def)
 apply simp
 apply clarify
@@ -307,9 +307,9 @@
   which may not hold 
 *}
 lemma err_semilat_UnionI:
-  "[| !A:AS. err_semilat(A, r, f); AS ~= {}; 
-      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] 
-  ==> err_semilat(Union AS, r, f)"
+  "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {}; 
+      !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk> 
+  \<Longrightarrow> err_semilat(Union AS, r, f)"
 apply (unfold semilat_def sl_def)
 apply (simp add: closed_err_Union_lift2I)
 apply (rule conjI)
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -17,31 +17,31 @@
   by (unfold super_def) (auto dest: subcls1D)
 
 constdefs
-  is_ref :: "ty => bool"
-  "is_ref T == case T of PrimT t => False | RefT r => True"
+  is_ref :: "ty \<Rightarrow> bool"
+  "is_ref T == case T of PrimT t \<Rightarrow> False | RefT r \<Rightarrow> True"
 
-  sup :: "'c prog => ty => ty => ty err"
+  sup :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty err"
   "sup G T1 T2 ==
-  case T1 of PrimT P1 => (case T2 of PrimT P2 => 
-                         (if P1 = P2 then OK (PrimT P1) else Err) | RefT R => Err)
-           | RefT R1 => (case T2 of PrimT P => Err | RefT R2 => 
-  (case R1 of NullT => (case R2 of NullT => OK NT | ClassT C => OK (Class C))
-            | ClassT C => (case R2 of NullT => OK (Class C) 
-                           | ClassT D => OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
+  case T1 of PrimT P1 \<Rightarrow> (case T2 of PrimT P2 \<Rightarrow> 
+                         (if P1 = P2 then OK (PrimT P1) else Err) | RefT R \<Rightarrow> Err)
+           | RefT R1 \<Rightarrow> (case T2 of PrimT P \<Rightarrow> Err | RefT R2 \<Rightarrow> 
+  (case R1 of NullT \<Rightarrow> (case R2 of NullT \<Rightarrow> OK NT | ClassT C \<Rightarrow> OK (Class C))
+            | ClassT C \<Rightarrow> (case R2 of NullT \<Rightarrow> OK (Class C) 
+                           | ClassT D \<Rightarrow> OK (Class (exec_lub (subcls1 G) (super G) C D)))))"
 
-  subtype :: "'c prog => ty => ty => bool"
+  subtype :: "'c prog \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"
   "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
 
-  is_ty :: "'c prog => ty => bool"
-  "is_ty G T == case T of PrimT P => True | RefT R =>
-               (case R of NullT => True | ClassT C => (C,Object):(subcls1 G)^*)"
+  is_ty :: "'c prog \<Rightarrow> ty \<Rightarrow> bool"
+  "is_ty G T == case T of PrimT P \<Rightarrow> True | RefT R \<Rightarrow>
+               (case R of NullT \<Rightarrow> True | ClassT C \<Rightarrow> (C,Object):(subcls1 G)^*)"
 
 
 translations
   "types G" == "Collect (is_type G)"
 
 constdefs
-  esl :: "'c prog => ty esl"
+  esl :: "'c prog \<Rightarrow> ty esl"
   "esl G == (types G, subtype G, sup G)"
 
 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
@@ -51,12 +51,12 @@
   by (auto elim: widen.elims)
 
 lemma is_tyI:
-  "[| is_type G T; wf_prog wf_mb G |] ==> is_ty G T"
+  "\<lbrakk> is_type G T; wf_prog wf_mb G \<rbrakk> \<Longrightarrow> is_ty G T"
   by (auto simp add: is_ty_def intro: subcls_C_Object 
            split: ty.splits ref_ty.splits)
 
 lemma is_type_conv: 
-  "wf_prog wf_mb G ==> is_type G T = is_ty G T"
+  "wf_prog wf_mb G \<Longrightarrow> is_type G T = is_ty G T"
 proof
   assume "is_type G T" "wf_prog wf_mb G" 
   thus "is_ty G T"
@@ -86,7 +86,7 @@
 qed
 
 lemma order_widen:
-  "acyclic (subcls1 G) ==> order (subtype G)"
+  "acyclic (subcls1 G) \<Longrightarrow> order (subtype G)"
   apply (unfold order_def lesub_def subtype_def)
   apply (auto intro: widen_trans)
   apply (case_tac x)
@@ -106,7 +106,7 @@
   done
 
 lemma wf_converse_subcls1_impl_acc_subtype:
-  "wf ((subcls1 G)^-1) ==> acc (subtype G)"
+  "wf ((subcls1 G)^-1) \<Longrightarrow> acc (subtype G)"
 apply (unfold acc_def lesssub_def)
 apply (drule_tac p = "(subcls1 G)^-1 - Id" in wf_subset)
  apply blast
@@ -159,8 +159,8 @@
 done 
 
 lemma closed_err_types:
-  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
-  ==> closed (err (types G)) (lift2 (sup G))"
+  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
+  \<Longrightarrow> closed (err (types G)) (lift2 (sup G))"
   apply (unfold closed_def plussub_def lift2_def sup_def)
   apply (auto split: err.split)
   apply (drule is_tyI, assumption)
@@ -171,9 +171,9 @@
 
 
 lemma sup_subtype_greater:
-  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
-      is_type G t1; is_type G t2; sup G t1 t2 = OK s |] 
-  ==> subtype G t1 s \<and> subtype G t2 s"
+  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
+      is_type G t1; is_type G t2; sup G t1 t2 = OK s \<rbrakk> 
+  \<Longrightarrow> subtype G t1 s \<and> subtype G t2 s"
 proof -
   assume wf_prog:       "wf_prog wf_mb G"
   assume single_valued: "single_valued (subcls1 G)" 
@@ -210,10 +210,10 @@
 qed
 
 lemma sup_subtype_smallest:
-  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
+  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
       is_type G a; is_type G b; is_type G c; 
-      subtype G a c; subtype G b c; sup G a b = OK d |]
-  ==> subtype G d c"
+      subtype G a c; subtype G b c; sup G a b = OK d \<rbrakk>
+  \<Longrightarrow> subtype G d c"
 proof -
   assume wf_prog:       "wf_prog wf_mb G"
   assume single_valued: "single_valued (subcls1 G)" 
@@ -244,7 +244,7 @@
   } note this [intro]
 
   have [dest!]:
-    "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
+    "\<And>C T. G \<turnstile> Class C \<preceq> T \<Longrightarrow> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
     by (frule widen_Class, auto)
 
   assume "is_type G a" "is_type G b" "is_type G c"
@@ -255,13 +255,13 @@
 qed
 
 lemma sup_exists:
-  "[| subtype G a c; subtype G b c; sup G a b = Err |] ==> False"
+  "\<lbrakk> subtype G a c; subtype G b c; sup G a b = Err \<rbrakk> \<Longrightarrow> False"
   by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def subtype_def
            split: ty.splits ref_ty.splits)
 
 lemma err_semilat_JType_esl_lemma:
-  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
-  ==> err_semilat (esl G)"
+  "\<lbrakk> wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) \<rbrakk> 
+  \<Longrightarrow> err_semilat (esl G)"
 proof -
   assume wf_prog:   "wf_prog wf_mb G"
   assume single_valued: "single_valued (subcls1 G)" 
@@ -297,12 +297,12 @@
 qed
 
 lemma single_valued_subcls1:
-  "wf_prog wf_mb G ==> single_valued (subcls1 G)"
+  "wf_prog wf_mb G \<Longrightarrow> single_valued (subcls1 G)"
   by (auto simp add: wf_prog_def unique_def single_valued_def
     intro: subcls1I elim!: subcls1.elims)
 
 theorem err_semilat_JType_esl:
-  "wf_prog wf_mb G ==> err_semilat (esl G)"
+  "wf_prog wf_mb G \<Longrightarrow> err_semilat (esl G)"
   by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
 
 end
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -14,8 +14,8 @@
   "exec G maxs rT et bs == 
   err_step (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"
 
-  kiljvm :: "jvm_prog => nat => nat => ty => exception_table => 
-             instr list => state list => state list"
+  kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
+             instr list \<Rightarrow> state list \<Rightarrow> state list"
   "kiljvm G maxs maxr rT et bs ==
   kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
 
@@ -28,7 +28,7 @@
         result = kiljvm G mxs (1+size pTs+mxl) rT et ins start
     in \<forall>n < size ins. result!n \<noteq> Err)"
 
-  wt_jvm_prog_kildall :: "jvm_prog => bool"
+  wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
   "wt_jvm_prog_kildall G ==
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G"
 
@@ -77,7 +77,7 @@
 
 
 theorem exec_pres_type:
-  "wf_prog wf_mb S ==> 
+  "wf_prog wf_mb S \<Longrightarrow> 
   pres_type (exec S maxs rT et bs) (size bs) (states S maxs maxr)"
   apply (unfold exec_def JVM_states_unfold)
   apply (rule pres_type_lift)
@@ -243,7 +243,7 @@
   by (unfold sup_state_opt_unfold) (blast dest: acyclic_subcls1 order_widen)
 
 theorem exec_mono:
-  "wf_prog wf_mb G ==>
+  "wf_prog wf_mb G \<Longrightarrow>
   mono (JVMType.le G maxs maxr) (exec G maxs rT et bs) (size bs) (states G maxs maxr)"  
   apply (unfold exec_def JVM_le_unfold JVM_states_unfold)  
   apply (rule mono_lift)
@@ -257,7 +257,7 @@
   done
 
 theorem semilat_JVM_slI:
-  "wf_prog wf_mb G ==> semilat (JVMType.sl G maxs maxr)"
+  "wf_prog wf_mb G \<Longrightarrow> semilat (JVMType.sl G maxs maxr)"
   apply (unfold JVMType.sl_def stk_esl_def reg_sl_def)
   apply (rule semilat_opt)
   apply (rule err_semilat_Product_esl)
@@ -275,7 +275,7 @@
 
 
 theorem is_bcv_kiljvm:
-  "[| wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) |] ==> 
+  "\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow> 
       is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs)
              (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)"
   apply (unfold kiljvm_def sl_triple_conv)
@@ -293,9 +293,9 @@
 
 
 theorem wt_kil_correct:
-  "[| wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G; 
-      is_class G C; \<forall>x \<in> set pTs. is_type G x |]
-  ==> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
+  "\<lbrakk> wt_kil G C pTs rT maxs mxl et bs; wf_prog wf_mb G; 
+      is_class G C; \<forall>x \<in> set pTs. is_type G x \<rbrakk>
+  \<Longrightarrow> \<exists>phi. wt_method G C pTs rT maxs mxl bs et phi"
 proof -
   let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
                 #(replicate (size bs - 1) (OK None))"
@@ -386,10 +386,10 @@
 
 
 theorem wt_kil_complete:
-  "[| wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
+  "\<lbrakk> wt_method G C pTs rT maxs mxl bs et phi; wf_prog wf_mb G; 
       length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x;
-      map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) |]
-  ==> wt_kil G C pTs rT maxs mxl et bs"
+      map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl)) \<rbrakk>
+  \<Longrightarrow> wt_kil G C pTs rT maxs mxl et bs"
 proof -
   assume wf: "wf_prog wf_mb G"  
   assume isclass: "is_class G C"
@@ -490,12 +490,12 @@
         have "JVMType.le G maxs ?maxr (OK None) (?phi!n)"
           by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def 
             split: err.splits)        
-        hence "[| n = Suc n'; n < length ?start |] 
-          ==> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
+        hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk> 
+          \<Longrightarrow> JVMType.le G maxs ?maxr (?start!n) (?phi!n)"
           by simp
       }
       ultimately
-      have "n < length ?start ==> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
+      have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?maxr) (?phi!n)"
         by (unfold lesub_def) (cases n, blast+)
     } 
     ultimately show ?thesis by (rule le_listI)
@@ -540,9 +540,9 @@
   programs without problems:
 *}
 lemma is_type_pTs:
-  "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
-      t \<in> set (snd sig) |]
-  ==> is_type G t"
+  "\<lbrakk> wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
+      t \<in> set (snd sig) \<rbrakk>
+  \<Longrightarrow> is_type G t"
 proof -
   assume "wf_prog wf_mb G" 
          "(C,S,fs,mdecls) \<in> set G"
@@ -559,7 +559,7 @@
 
 
 theorem jvm_kildall_correct:
-  "wt_jvm_prog_kildall G ==> \<exists>Phi. wt_jvm_prog G Phi"
+  "wt_jvm_prog_kildall G \<Longrightarrow> \<exists>Phi. wt_jvm_prog G Phi"
 proof -  
   assume wtk: "wt_jvm_prog_kildall G"
 
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -15,58 +15,58 @@
   state_type   = "opstack_type \<times> locvars_type"
   state        = "state_type option err"    -- "for Kildall"
   method_type  = "state_type option list"   -- "for BVSpec"
-  class_type   = "sig => method_type"
-  prog_type    = "cname => class_type"
+  class_type   = "sig \<Rightarrow> method_type"
+  prog_type    = "cname \<Rightarrow> class_type"
 
 
 constdefs
-  stk_esl :: "'c prog => nat => ty list esl"
+  stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl"
   "stk_esl S maxs == upto_esl maxs (JType.esl S)"
 
-  reg_sl :: "'c prog => nat => ty err list sl"
+  reg_sl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty err list sl"
   "reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"
 
-  sl :: "'c prog => nat => nat => state sl"
+  sl :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state sl"
   "sl S maxs maxr ==
   Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"
 
 constdefs
-  states :: "'c prog => nat => nat => state set"
+  states :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state set"
   "states S maxs maxr == fst(sl S maxs maxr)"
 
-  le :: "'c prog => nat => nat => state ord"
+  le :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state ord"
   "le S maxs maxr == fst(snd(sl S maxs maxr))"
 
-  sup :: "'c prog => nat => nat => state binop"
+  sup :: "'c prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state binop"
   "sup S maxs maxr == snd(snd(sl S maxs maxr))"
 
 
 constdefs
-  sup_ty_opt :: "['code prog,ty err,ty err] => bool" 
+  sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" 
                  ("_ |- _ <=o _" [71,71] 70)
   "sup_ty_opt G == Err.le (subtype G)"
 
-  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
+  sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
               ("_ |- _ <=l _"  [71,71] 70)
   "sup_loc G == Listn.le (sup_ty_opt G)"
 
-  sup_state :: "['code prog,state_type,state_type] => bool"   
+  sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"   
                ("_ |- _ <=s _"  [71,71] 70)
   "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
 
-  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
+  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
                    ("_ |- _ <=' _"  [71,71] 70)
   "sup_state_opt G == Opt.le (sup_state G)"
 
 
 syntax (xsymbols)
-  sup_ty_opt    :: "['code prog,ty err,ty err] => bool" 
+  sup_ty_opt    :: "['code prog,ty err,ty err] \<Rightarrow> bool" 
                    ("_ \<turnstile> _ <=o _" [71,71] 70)
-  sup_loc       :: "['code prog,locvars_type,locvars_type] => bool" 
+  sup_loc       :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
                    ("_ \<turnstile> _ <=l _" [71,71] 70)
-  sup_state     :: "['code prog,state_type,state_type] => bool" 
+  sup_state     :: "['code prog,state_type,state_type] \<Rightarrow> bool" 
                    ("_ \<turnstile> _ <=s _" [71,71] 70)
-  sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
+  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
                    ("_ \<turnstile> _ <=' _" [71,71] 70)
                    
 
@@ -98,7 +98,7 @@
              sup_ty_opt_def JVM_le_unfold) simp
 
 lemma zip_map [rule_format]:
-  "\<forall>a. length a = length b --> 
+  "\<forall>a. length a = length b \<longrightarrow> 
   zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)"
   apply (induct b) 
    apply simp
@@ -188,11 +188,11 @@
   by (simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def)
 
 theorem sup_ty_opt_OK:
-  "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x"
+  "G \<turnstile> a <=o (OK b) \<Longrightarrow> \<exists> x. a = OK x"
   by (clarsimp simp add: sup_ty_opt_def Err.le_def split: err.splits)
 
 lemma widen_PrimT_conv1 [simp]:
-  "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
+  "\<lbrakk> G \<turnstile> S \<preceq> T; S = PrimT x\<rbrakk> \<Longrightarrow> T = PrimT x"
   by (auto elim: widen.elims)
 
 theorem sup_PTS_eq:
@@ -214,20 +214,20 @@
 
 
 theorem sup_loc_length:
-  "G \<turnstile> a <=l b ==> length a = length b"
+  "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
 proof -
   assume G: "G \<turnstile> a <=l b"
-  have "\<forall>b. (G \<turnstile> a <=l b) --> length a = length b"
+  have "\<forall>b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
     by (induct a, auto)
   with G
   show ?thesis by blast
 qed
 
 theorem sup_loc_nth:
-  "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
+  "\<lbrakk> G \<turnstile> a <=l b; n < length a \<rbrakk> \<Longrightarrow> G \<turnstile> (a!n) <=o (b!n)"
 proof -
   assume a: "G \<turnstile> a <=l b" "n < length a"
-  have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))"
+  have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
     (is "?P a")
   proof (induct a)
     show "?P []" by simp
@@ -248,8 +248,8 @@
 qed
 
 theorem all_nth_sup_loc:
-  "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) 
-  --> (G \<turnstile> a <=l b)" (is "?P a")
+  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) 
+  \<longrightarrow> (G \<turnstile> a <=l b)" (is "?P a")
 proof (induct a)
   show "?P []" by simp
 
@@ -258,14 +258,14 @@
   show "?P (l#ls)"
   proof (intro strip)
     fix b
-    assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
+    assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
     assume l: "length (l#ls) = length b"
     
     then obtain b' bs where b: "b = b'#bs"
       by - (cases b, simp, simp add: neq_Nil_conv, rule that)
 
     with f
-    have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))"
+    have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
       by auto
 
     with f b l IH
@@ -276,12 +276,12 @@
 
 
 theorem sup_loc_append:
-  "length a = length b ==> 
+  "length a = length b \<Longrightarrow> 
    (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
 proof -
   assume l: "length a = length b"
 
-  have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
+  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
             (G \<turnstile> x <=l y))" (is "?P a") 
   proof (induct a)
     show "?P []" by simp
@@ -347,7 +347,7 @@
 
 
 theorem sup_loc_update [rule_format]:
-  "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> 
+  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
           (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
 proof (induct x)
   show "?P []" by simp
@@ -365,17 +365,17 @@
 
 
 theorem sup_state_length [simp]:
-  "G \<turnstile> s2 <=s s1 ==> 
+  "G \<turnstile> s2 <=s s1 \<Longrightarrow> 
    length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
   by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def);
 
 theorem sup_state_append_snd:
-  "length a = length b ==> 
+  "length a = length b \<Longrightarrow> 
   (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
 
 theorem sup_state_append_fst:
-  "length a = length b ==> 
+  "length a = length b \<Longrightarrow> 
   (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append)
 
@@ -390,13 +390,13 @@
   by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons sup_loc_Cons2)
 
 theorem sup_state_ignore_fst:  
-  "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)"
+  "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
   by (simp add: sup_state_def lesub_def Product.le_def)
 
 theorem sup_state_rev_fst:
   "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
 proof -
-  have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
+  have m: "\<And>f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
   show ?thesis by (simp add: m sup_state_def stk_convert lesub_def Product.le_def)
 qed
   
@@ -423,17 +423,17 @@
 
 
 theorem sup_ty_opt_trans [trans]:
-  "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c"
+  "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
   by (auto intro: widen_trans 
            simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def 
            split: err.splits)
 
 theorem sup_loc_trans [trans]:
-  "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c"
+  "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
 proof -
   assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
  
-  hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))"
+  hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
   proof (intro strip)
     fix n 
     assume n: "n < length a"
@@ -442,7 +442,7 @@
       by - (rule sup_loc_nth)
     also 
     from n G
-    have "G \<turnstile> ... <=o (c!n)"
+    have "G \<turnstile> \<dots> <=o (c!n)"
       by - (rule sup_loc_nth, auto dest: sup_loc_length)
     finally
     show "G \<turnstile> (a!n) <=o (c!n)" .
@@ -455,11 +455,11 @@
   
 
 theorem sup_state_trans [trans]:
-  "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c"
+  "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
   by (auto intro: sup_loc_trans simp add: sup_state_def stk_convert Product.le_def lesub_def)
 
 theorem sup_state_opt_trans [trans]:
-  "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c"
+  "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
   by (auto intro: sup_state_trans 
            simp add: sup_state_opt_def Opt.le_def lesub_def 
            split: option.splits)
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Kildall.thy
--- a/src/HOL/MicroJava/BV/Kildall.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Kildall.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -11,24 +11,24 @@
 theory Kildall = Typing_Framework + While_Combinator + Product:
 
 
-syntax "@lesubstep_type" :: "(nat \<times> 's) list => 's ord => (nat \<times> 's) list => bool"
+syntax "@lesubstep_type" :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
        ("(_ /<=|_| _)" [50, 0, 51] 50)
 translations
  "x <=|r| y" == "x <=[(Product.le (op =) r)] y"
  
 
 constdefs
- pres_type :: "'s step_type => nat => 's set => bool"
+ pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
 "pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
 
- mono :: "'s ord => 's step_type => nat => 's set => bool"
+ mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
 "mono r step n A ==
- \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t --> step p s <=|r| step p t"
+ \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
 
 consts
  iter :: "'s binop \<Rightarrow> 's step_type \<Rightarrow>
           's list \<Rightarrow> nat set \<Rightarrow> 's list \<times> nat set"
- propa :: "'s binop => (nat \<times> 's) list => 's list => nat set => 's list * nat set"
+ propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set"
 
 primrec
 "propa f []      ss w = (ss,w)"
@@ -45,13 +45,13 @@
        (ss,w)"
 
 constdefs
- unstables :: "'s ord => 's step_type => 's list => nat set"
+ unstables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat set"
 "unstables r step ss == {p. p < size ss \<and> \<not>stable r step ss p}"
 
- kildall :: "'s ord => 's binop => 's step_type => 's list => 's list"
+ kildall :: "'s ord \<Rightarrow> 's binop \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> 's list"
 "kildall r f step ss == fst(iter f step ss (unstables r step ss))"
 
-consts merges :: "'s binop => (nat \<times> 's) list => 's list => 's list"
+consts merges :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> 's list"
 primrec
 "merges f []      ss = ss"
 "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
@@ -61,16 +61,16 @@
 
 
 consts
- "@plusplussub" :: "'a list => ('a => 'a => 'a) => 'a => 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
+ "@plusplussub" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
 primrec
   "[] ++_f y = y"
   "(x#xs) ++_f y = xs ++_f (x +_f y)"
 
 lemma nth_merges:
-  "!!ss. [| semilat (A, r, f); p < length ss; ss \<in> list n A; 
-            \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A |] ==>
+  "\<And>ss. \<lbrakk> semilat (A, r, f); p < length ss; ss \<in> list n A; 
+            \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
   (merges f ps ss)!p = map snd [(p',t') \<in> ps. p'=p] ++_f ss!p"
-  (is "!!ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
+  (is "\<And>ss. _ \<Longrightarrow> _ \<Longrightarrow> _ \<Longrightarrow> ?steptype ps \<Longrightarrow> ?P ss ps")
 proof (induct ps)
   show "\<And>ss. ?P ss []" by simp
 
@@ -98,15 +98,15 @@
 
 
 lemma pres_typeD:
-  "[| pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) |] ==> s' \<in> A"
+  "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
   by (unfold pres_type_def, blast)
 
 lemma boundedD: 
-  "[| bounded step n; p < n; (q,t) : set (step p xs) |] ==> q < n" 
+  "\<lbrakk> bounded step n; p < n; (q,t) : set (step p xs) \<rbrakk> \<Longrightarrow> q < n" 
   by (unfold bounded_def, blast)
 
 lemma monoD:
-  "[| mono r step n A; p < n; s\<in>A; s <=_r t |] ==> step p s <=|r| step p t"
+  "\<lbrakk> mono r step n A; p < n; s\<in>A; s <=_r t \<rbrakk> \<Longrightarrow> step p s <=|r| step p t"
   by (unfold mono_def, blast)
 
 (** merges **)
@@ -117,9 +117,9 @@
 
 
 lemma merges_preserves_type_lemma: 
-  "[| semilat(A,r,f) |] ==>
-     \<forall>xs. xs \<in> list n A --> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
-          --> merges f ps xs \<in> list n A" 
+  "semilat(A,r,f) \<Longrightarrow>
+     \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
+          \<longrightarrow> merges f ps xs \<in> list n A" 
   apply (frule semilatDclosedI) 
   apply (unfold closed_def) 
   apply (induct_tac ps)
@@ -128,13 +128,13 @@
   done
 
 lemma merges_preserves_type [simp]:
-  "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A |]
-  ==> merges f ps xs \<in> list n A"
+  "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
+  \<Longrightarrow> merges f ps xs \<in> list n A"
   by (simp add: merges_preserves_type_lemma)
   
 lemma merges_incr_lemma:
-  "[| semilat(A,r,f) |] ==> 
-     \<forall>xs. xs \<in> list n A --> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) --> xs <=[r] merges f ps xs"
+  "semilat(A,r,f) \<Longrightarrow> 
+     \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
   apply (induct_tac ps)
    apply simp
   apply simp
@@ -149,14 +149,14 @@
   done
 
 lemma merges_incr:
-  "[| semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A |] 
-  ==> xs <=[r] merges f ps xs"
+  "\<lbrakk> semilat(A,r,f); xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
+  \<Longrightarrow> xs <=[r] merges f ps xs"
   by (simp add: merges_incr_lemma)
 
 
 lemma merges_same_conv [rule_format]:
-  "[| semilat(A,r,f) |] ==> 
-     (\<forall>xs. xs \<in> list n A --> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) --> 
+  "semilat(A,r,f) \<Longrightarrow> 
+     (\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
      (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
   apply (induct_tac ps)
    apply simp
@@ -191,25 +191,25 @@
 
 
 lemma list_update_le_listI [rule_format]:
-  "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->  
-   x <=_r ys!p --> semilat(A,r,f) --> x\<in>A --> 
+  "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
+   x <=_r ys!p \<longrightarrow> semilat(A,r,f) \<longrightarrow> x\<in>A \<longrightarrow> 
    xs[p := x +_f xs!p] <=[r] ys"
   apply (unfold Listn.le_def lesub_def semilat_def)
   apply (simp add: list_all2_conv_all_nth nth_list_update)
   done
 
 lemma merges_pres_le_ub:
-  "[| semilat(A,r,f); set ts <= A; set ss <= A; 
+  "\<lbrakk> semilat(A,r,f); set ts <= A; set ss <= A; 
      \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts; 
-     ss <=[r] ts |] 
-  ==> merges f ps ss <=[r] ts"
+     ss <=[r] ts \<rbrakk> 
+  \<Longrightarrow> merges f ps ss <=[r] ts"
 proof -
   { fix A r f t ts ps
     have
-    "!!qs. [| semilat(A,r,f); set ts <= A; 
-              \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts |] ==> 
-    set qs <= set ps  --> 
-    (\<forall>ss. set ss <= A --> ss <=[r] ts --> merges f qs ss <=[r] ts)"
+    "\<And>qs. \<lbrakk> semilat(A,r,f); set ts <= A; 
+              \<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts \<rbrakk> \<Longrightarrow> 
+    set qs <= set ps  \<longrightarrow> 
+    (\<forall>ss. set ss <= A \<longrightarrow> ss <=[r] ts \<longrightarrow> merges f qs ss <=[r] ts)"
     apply (induct_tac qs)
      apply simp
     apply (simp (no_asm_simp))
@@ -233,7 +233,7 @@
 
 
 lemma decomp_propa:
-  "!!ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
+  "\<And>ss w. (\<forall>(q,t)\<in>set qs. q < size ss) \<Longrightarrow> 
    propa f qs ss w = 
    (merges f qs ss, {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un w)"
   apply (induct qs)
@@ -263,7 +263,7 @@
   thus "(x#xs) ++_f y \<in> A" by simp
 qed
 
-lemma ub2: "!!y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
+lemma ub2: "\<And>y. \<lbrakk>semilat (A, r, f); set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
 proof (induct x)
   show "\<And>y. semilat(A, r, f) \<Longrightarrow> y <=_r [] ++_f y" by simp 
   
@@ -287,7 +287,8 @@
 qed
 
 
-lemma ub1: "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+lemma ub1: 
+  "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
 proof (induct ls)
   show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
   
@@ -298,7 +299,8 @@
   then obtain s: "s \<in> A" and ls: "set ls \<subseteq> A" by simp
   assume y: "y \<in> A" 
 
-  assume "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
+  assume 
+    "\<And>y. \<lbrakk>semilat (A, r, f); set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
   hence IH: "\<And>y. x \<in> set ls \<Longrightarrow> y \<in> A \<Longrightarrow> x <=_r ls ++_f y" .
 
   assume "x \<in> set (s#ls)"
@@ -356,12 +358,12 @@
 
 
 lemma stable_pres_lemma:
-  "[| semilat (A,r,f); pres_type step n A; bounded step n; 
+  "\<lbrakk> semilat (A,r,f); pres_type step n A; bounded step n; 
      ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
      \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
      \<forall>s'. (q,s') \<in> set (step p (ss ! p)) \<longrightarrow> s' +_f ss ! q = ss ! q; 
-     q \<notin> w \<or> q = p |] 
-  ==> stable r step (merges f (step p (ss!p)) ss) q"
+     q \<notin> w \<or> q = p \<rbrakk> 
+  \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
   apply (unfold stable_def)
   apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
    prefer 2
@@ -434,7 +436,7 @@
  
   
 lemma lesub_step_type:
-  "!!b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
+  "\<And>b x y. a <=|r| b \<Longrightarrow> (x,y) \<in> set a \<Longrightarrow> \<exists>y'. (x, y') \<in> set b \<and> y <=_r y'"
 apply (induct a)
  apply simp
 apply simp
@@ -451,10 +453,10 @@
 
 
 lemma merges_bounded_lemma:
-  "[| semilat (A,r,f); mono r step n A; bounded step n; 
+  "\<lbrakk> semilat (A,r,f); mono r step n A; bounded step n; 
      \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
-     ss <=[r] ts; ! p. p < n --> stable r step ts p |] 
-  ==> merges f (step p (ss!p)) ss <=[r] ts"
+     ss <=[r] ts; ! p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
+  \<Longrightarrow> merges f (step p (ss!p)) ss <=[r] ts"
   apply (unfold stable_def)
   apply (rule merges_pres_le_ub)
       apply assumption
@@ -481,7 +483,7 @@
   done
 
 lemma termination_lemma:  
-  "[| semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w |] ==> 
+  "\<lbrakk> semilat(A,r,f); ss \<in> list n A; \<forall>(q,t)\<in>set qs. q<n \<and> t\<in>A; p\<in>w \<rbrakk> \<Longrightarrow> 
       ss <[r] merges f qs ss \<or> 
   merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w"
   apply (unfold lesssub_def)
@@ -617,10 +619,10 @@
 done
 
 lemma is_bcv_kildall:
-  "[| semilat(A,r,f); acc r; top r T; 
+  "\<lbrakk> semilat(A,r,f); acc r; top r T; 
       pres_type step n A; bounded step n; 
-      mono r step n A |]
-  ==> is_bcv r T step n A (kildall r f step)"
+      mono r step n A \<rbrakk>
+  \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
 apply(unfold is_bcv_def wt_step_def)
 apply(insert kildall_properties[of A])
 apply(simp add:stables_def)
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -14,43 +14,43 @@
 theory LBVComplete = BVSpec + LBVSpec + EffectMono:
 
 constdefs
-  contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
+  contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
   "contains_targets ins cert phi pc == 
      \<forall>pc' \<in> set (succs (ins!pc) pc). 
-      pc' \<noteq> pc+1 \<and> pc' < length ins --> cert!pc' = phi!pc'"
+      pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
 
-  fits :: "[instr list, certificate, method_type] => bool"
-  "fits ins cert phi == \<forall>pc. pc < length ins --> 
+  fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
+  "fits ins cert phi == \<forall>pc. pc < length ins \<longrightarrow> 
                        contains_targets ins cert phi pc \<and>
                        (cert!pc = None \<or> cert!pc = phi!pc)"
 
-  is_target :: "[instr list, p_count] => bool" 
+  is_target :: "[instr list, p_count] \<Rightarrow> bool" 
   "is_target ins pc == 
      \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
 
 
 constdefs 
-  make_cert :: "[instr list, method_type] => certificate"
+  make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
   "make_cert ins phi == 
      map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
 
-  make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
+  make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
   "make_Cert G Phi ==  \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig)
                                 in make_cert b (Phi C sig)"
   
 lemmas [simp del] = split_paired_Ex
 
 lemma make_cert_target:
-  "[| pc < length ins; is_target ins pc |] ==> make_cert ins phi ! pc = phi!pc"
+  "\<lbrakk> pc < length ins; is_target ins pc \<rbrakk> \<Longrightarrow> make_cert ins phi ! pc = phi!pc"
   by (simp add: make_cert_def)
 
 lemma make_cert_approx:
-  "[| pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc |] ==> 
+  "\<lbrakk> pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc \<rbrakk> \<Longrightarrow> 
    make_cert ins phi ! pc = None"
   by (auto simp add: make_cert_def)
 
 lemma make_cert_contains_targets:
-  "pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc"
+  "pc < length ins \<Longrightarrow> contains_targets ins (make_cert ins phi) phi pc"
 proof (unfold contains_targets_def, intro strip, elim conjE) 
   fix pc'
   assume "pc < length ins" 
@@ -71,19 +71,19 @@
   by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
 
 lemma fitsD: 
-  "[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); 
-      pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
-  ==> cert!pc' = phi!pc'"
+  "\<lbrakk> fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); 
+      pc' \<noteq> Suc pc; pc < length ins; pc' < length ins \<rbrakk>
+  \<Longrightarrow> cert!pc' = phi!pc'"
   by (clarsimp simp add: fits_def contains_targets_def)
 
 lemma fitsD2:
-   "[| fits ins cert phi; pc < length ins; cert!pc = Some s |]
-  ==> cert!pc = phi!pc"
+   "\<lbrakk> fits ins cert phi; pc < length ins; cert!pc = Some s \<rbrakk>
+  \<Longrightarrow> cert!pc = phi!pc"
   by (auto simp add: fits_def)
                            
 lemma wtl_inst_mono:
-  "[| wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
-      pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+  "\<lbrakk> wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
+      pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow>
   \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
 proof -
   assume pc:   "pc < length ins" "i = ins!pc"
@@ -144,8 +144,8 @@
 
 
 lemma wtl_cert_mono:
-  "[| wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
-      pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+  "\<lbrakk> wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; 
+      pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow>
   \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
 proof -
   assume wtl:  "wtl_cert i G rT s1 cert mxs mpc pc = OK s1'" and
@@ -181,8 +181,8 @@
 
  
 lemma wt_instr_imp_wtl_inst:
-  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
-      pc < length ins; length ins = max_pc |] ==> 
+  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
+      pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
   wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
  proof -
   assume wt:   "wt_instr (ins!pc) G rT phi mxs max_pc pc" 
@@ -193,14 +193,14 @@
   have app: "app (ins!pc) G mxs rT (phi!pc)" by (simp add: wt_instr_def)
 
   from wt pc
-  have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
+  have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) \<Longrightarrow> pc' < length ins"
     by (simp add: wt_instr_def)
 
   let ?s' = "eff (ins!pc) G (phi!pc)"
 
   from wt fits pc
-  have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|] 
-    ==> G \<turnstile> ?s' <=' cert!pc'"
+  have cert: "\<And>pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
+    \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
     by (auto dest: fitsD simp add: wt_instr_def)     
 
   from app pc cert pc'
@@ -209,9 +209,9 @@
 qed
 
 lemma wt_less_wtl:
-  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; 
+  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; 
       wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
-      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
+      fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
   G \<turnstile> s <=' phi ! Suc pc"
 proof -
   assume wt:   "wt_instr (ins!pc) G rT phi mxs max_pc pc" 
@@ -222,7 +222,7 @@
   { assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
     with wtl have "s = eff (ins!pc) G (phi!pc)"
       by (simp add: wtl_inst_OK)
-    also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
+    also from suc wt have "G \<turnstile> \<dots> <=' phi!Suc pc"
       by (simp add: wt_instr_def)
     finally have ?thesis .
   }
@@ -244,8 +244,8 @@
   
 
 lemma wt_instr_imp_wtl_cert:
-  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
-      pc < length ins; length ins = max_pc |] ==> 
+  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi;
+      pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
   wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
 proof -
   assume "wt_instr (ins!pc) G rT phi mxs max_pc pc" and 
@@ -256,7 +256,7 @@
   hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err"
     by (rule wt_instr_imp_wtl_inst)
 
-  hence "cert!pc = None ==> ?thesis"
+  hence "cert!pc = None \<Longrightarrow> ?thesis"
     by (simp add: wtl_cert_def)
 
   moreover
@@ -276,9 +276,9 @@
   
 
 lemma wt_less_wtl_cert:
-  "[| wt_instr (ins!pc) G rT phi mxs max_pc pc; 
+  "\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; 
       wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s;
-      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
+      fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> 
   G \<turnstile> s <=' phi ! Suc pc"
 proof -
   assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s"
@@ -319,14 +319,14 @@
 *}
 
 theorem wt_imp_wtl_inst_list:
-"\<forall> pc. (\<forall>pc'. pc' < length all_ins --> 
-        wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') -->
-       fits all_ins cert phi --> 
-       (\<exists>l. pc = length l \<and> all_ins = l@ins) -->  
-       pc < length all_ins -->      
-       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) --> 
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> 
+        wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') \<longrightarrow>
+       fits all_ins cert phi \<longrightarrow> 
+       (\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow>  
+       pc < length all_ins \<longrightarrow>      
+       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow> 
              wtl_inst_list ins G rT cert mxs (length all_ins) pc s \<noteq> Err)" 
-(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"  
+(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"  
  is "\<forall>pc. ?C pc ins" is "?P ins") 
 proof (induct "?P" "ins")
   case Nil
@@ -338,7 +338,7 @@
   show "?P (i#ins')" 
   proof (intro allI impI, elim exE conjE)
     fix pc s l
-    assume wt  : "\<forall>pc'. pc' < length all_ins --> 
+    assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
                         wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc'"
     assume fits: "fits all_ins cert phi"
     assume l   : "pc < length all_ins"
@@ -357,7 +357,7 @@
     from Cons
     have "?C (Suc pc) ins'" by blast
     with wt fits pc
-    have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
+    have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
 
     show "wtl_inst_list (i#ins') G rT cert mxs (length all_ins) pc s \<noteq> Err" 
     proof (cases "?len (Suc pc)")
@@ -398,15 +398,15 @@
   
 
 lemma fits_imp_wtl_method_complete:
-  "[| wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi |] 
-  ==> wtl_method G C pTs rT mxs mxl ins cert"
+  "\<lbrakk> wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi \<rbrakk> 
+  \<Longrightarrow> wtl_method G C pTs rT mxs mxl ins cert"
 by (simp add: wt_method_def wtl_method_def)
    (rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) 
 
 
 lemma wtl_method_complete:
   "wt_method G C pTs rT mxs mxl ins phi 
-  ==> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
+  \<Longrightarrow> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)"
 proof -
   assume "wt_method G C pTs rT mxs mxl ins phi" 
   moreover
@@ -419,7 +419,7 @@
 
 
 theorem wtl_complete:
-  "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
+  "wt_jvm_prog G Phi \<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)"
 proof -
   assume wt: "wt_jvm_prog G Phi"
    
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -17,40 +17,40 @@
 lemmas [simp del] = split_paired_Ex split_paired_All
 
 constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => bool"
+fits :: "[method_type,instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> bool"
 "fits phi is G rT s0 maxs maxr et cert == 
-  (\<forall>pc s1. pc < length is -->
-    (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 -->
-    (case cert!pc of None   => phi!pc = s1
-                   | Some t => phi!pc = Some t)))"
+  (\<forall>pc s1. pc < length is \<longrightarrow>
+    (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0 = OK s1 \<longrightarrow>
+    (case cert!pc of None   \<Rightarrow> phi!pc = s1
+                   | Some t \<Rightarrow> phi!pc = Some t)))"
 
 constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] => method_type"
+make_phi :: "[instr list,jvm_prog,ty,state_type option,nat,nat,exception_table,certificate] \<Rightarrow> method_type"
 "make_phi is G rT s0 maxs maxr et cert == 
    map (\<lambda>pc. case cert!pc of 
-               None   => ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0) 
-             | Some t => Some t) [0..length is(]"
+               None   \<Rightarrow> ok_val (wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s0) 
+             | Some t \<Rightarrow> Some t) [0..length is(]"
 
 
 lemma fitsD_None:
-  "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
+  "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
     wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1; 
-    cert ! pc = None|] ==> phi!pc = s1"
+    cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
   by (auto simp add: fits_def)
 
 lemma fitsD_Some:
-  "[|fits phi is G rT s0 mxs mxr et cert; pc < length is;
+  "\<lbrakk>fits phi is G rT s0 mxs mxr et cert; pc < length is;
     wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0 = OK s1; 
-    cert ! pc = Some t|] ==> phi!pc = Some t"
+    cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
   by (auto simp add: fits_def)
 
 lemma make_phi_Some:
-  "[| pc < length is; cert!pc = Some t |] ==> 
+  "\<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> 
   make_phi is G rT s0 mxs mxr et cert ! pc = Some t"
   by (simp add: make_phi_def)
 
 lemma make_phi_None:
-  "[| pc < length is; cert!pc = None |] ==> 
+  "\<lbrakk> pc < length is; cert!pc = None \<rbrakk> \<Longrightarrow> 
   make_phi is G rT s0 mxs mxr et cert ! pc = 
   ok_val (wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s0)"
   by (simp add: make_phi_def)
@@ -65,8 +65,8 @@
 qed
   
 lemma fits_lemma1:
-  "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'; fits phi is G rT s mxs mxr et cert |]
-  ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
+  "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'; fits phi is G rT s mxs mxr et cert \<rbrakk>
+  \<Longrightarrow> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
 proof (intro strip)
   fix pc t 
   assume "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s = OK s'"
@@ -83,10 +83,10 @@
 
 
 lemma wtl_suc_pc:
- "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
+ "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err;
      wtl_inst_list (take pc is) G rT cert mxs mxr (length is) et 0 s = OK s';
      wtl_cert (is!pc) G rT s' cert mxs mxr (length is) et pc = OK s'';
-     fits phi is G rT s mxs mxr et cert; Suc pc < length is |] ==>
+     fits phi is G rT s mxs mxr et cert; Suc pc < length is \<rbrakk> \<Longrightarrow>
   G \<turnstile> s'' <=' phi ! Suc pc"
 proof -
   
@@ -117,15 +117,15 @@
     "wtl_cert l G rT s'' cert mxs mxr (length is) et (Suc pc) = OK x"
     by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
 
-  hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
+  hence c1: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> G \<turnstile> s'' <=' cert!Suc pc"
     by (simp add: wtl_cert_def split: split_if_asm)
   moreover
   from fits pc wts
-  have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
+  have c2: "\<And>t. cert!Suc pc = Some t \<Longrightarrow> phi!Suc pc = cert!Suc pc"
     by - (drule fitsD_Some, auto)
   moreover
   from fits pc wts
-  have c3: "cert!Suc pc = None ==> phi!Suc pc = s''"
+  have c3: "cert!Suc pc = None \<Longrightarrow> phi!Suc pc = s''"
     by (rule fitsD_None)
   ultimately
   show ?thesis by (cases "cert!Suc pc", auto)
@@ -133,8 +133,8 @@
 
 
 lemma wtl_fits_wt:
-  "[| wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
-      fits phi is G rT s mxs mxr et cert; pc < length is |] ==>
+  "\<lbrakk> wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
+      fits phi is G rT s mxs mxr et cert; pc < length is \<rbrakk> \<Longrightarrow>
    wt_instr (is!pc) G rT phi mxs (length is) et pc"
 proof -
   assume fits: "fits phi is G rT s mxs mxr et cert"
@@ -146,10 +146,10 @@
     by - (drule wtl_all, auto)
 
   from fits wtl pc have cert_Some: 
-    "!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
+    "\<And>t pc. \<lbrakk> pc < length is; cert!pc = Some t \<rbrakk> \<Longrightarrow> phi!pc = Some t"
     by (auto dest: fits_lemma1)
   
-  from fits wtl pc have cert_None: "cert!pc = None ==> phi!pc = s'"
+  from fits wtl pc have cert_None: "cert!pc = None \<Longrightarrow> phi!pc = s'"
     by - (drule fitsD_None)
   
   from pc c cert_None cert_Some
@@ -169,8 +169,8 @@
       case False          
       with wti pc'
       have G: "G \<turnstile> r <=' cert ! pc'" by (simp add: wtl_inst_OK) blast
-      hence "cert!pc' = None ==> r = None" by simp
-      hence "cert!pc' = None ==> ?thesis" by simp
+      hence "cert!pc' = None \<Longrightarrow> r = None" by simp
+      hence "cert!pc' = None \<Longrightarrow> ?thesis" by simp
       moreover {
         fix t assume "cert!pc' = Some t"
         with less have "phi!pc' = cert!pc'" by (simp add: cert_Some)
@@ -183,7 +183,7 @@
       have "G \<turnstile> r <=' s''"  sorry
       also
       from wtl w fits c pc 
-      have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc" 
+      have "Suc pc < length is \<Longrightarrow> G \<turnstile> s'' <=' phi ! Suc pc" 
         by - (rule wtl_suc_pc)
       with True less
       have "G \<turnstile> s'' <=' phi ! Suc pc" by blast
@@ -197,8 +197,8 @@
 
     
 lemma fits_first:
-  "[| 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
-      fits phi is G rT s mxs mxr et cert |] ==> 
+  "\<lbrakk> 0 < length is; wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err; 
+      fits phi is G rT s mxs mxr et cert \<rbrakk> \<Longrightarrow> 
   G \<turnstile> s <=' phi ! 0"
 proof -
   assume wtl:  "wtl_inst_list is G rT cert mxs mxr (length is) et 0 s \<noteq> Err"
@@ -210,11 +210,11 @@
     by simp
   
   with fits pc
-  have "cert!0 = None ==> phi!0 = s"
+  have "cert!0 = None \<Longrightarrow> phi!0 = s"
     by (rule fitsD_None)
   moreover    
   from fits pc wt0
-  have "!!t. cert!0 = Some t ==> phi!0 = cert!0"
+  have "\<And>t. cert!0 = Some t \<Longrightarrow> phi!0 = cert!0"
     by - (drule fitsD_Some, auto)
   moreover
   from pc
@@ -225,7 +225,7 @@
     "wtl_cert x G rT s cert mxs mxr (length is) et 0 = OK s'"
     by auto
   hence 
-    "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
+    "\<And>t. cert!0 = Some t \<Longrightarrow> G \<turnstile> s <=' cert!0"
     by (simp add: wtl_cert_def split: split_if_asm)
 
   ultimately
@@ -235,7 +235,7 @@
 
   
 lemma wtl_method_correct:
-"wtl_method G C pTs rT mxs mxl et ins cert ==> \<exists> phi. wt_method G C pTs rT mxs mxl ins et phi"
+"wtl_method G C pTs rT mxs mxl et ins cert \<Longrightarrow> \<exists> phi. wt_method G C pTs rT mxs mxl ins et phi"
 proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
   let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
   assume pc:  "0 < length ins"
@@ -246,7 +246,7 @@
 
   with wtl
   have allpc:
-    "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
+    "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi mxs (length ins) et pc"
     by (blast intro: wtl_fits_wt)
 
   from pc wtl fits
@@ -259,7 +259,7 @@
 
 
 theorem wtl_correct:
-  "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
+  "wtl_jvm_prog G cert \<Longrightarrow> \<exists> Phi. wt_jvm_prog G Phi"
 proof -  
   assume wtl: "wtl_jvm_prog G cert"
 
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -22,8 +22,8 @@
 
 types
   certificate       = "state_type option list" 
-  class_certificate = "sig => certificate"
-  prog_certificate  = "cname => class_certificate"
+  class_certificate = "sig \<Rightarrow> certificate"
+  prog_certificate  = "cname \<Rightarrow> class_certificate"
 
 consts
   merge :: "[jvm_prog, p_count, nat, nat, p_count, certificate, (nat \<times> (state_type option)) list, state] \<Rightarrow> state"
@@ -38,24 +38,24 @@
 
 constdefs 
   wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
-               => state_type option err" 
+               \<Rightarrow> state_type option err" 
   "wtl_inst i G rT s cert maxs maxr max_pc et pc == 
      if app i G maxs rT pc et s then 
        merge G pc maxs maxr max_pc cert (eff i G pc et s) (OK (cert!(pc+1)))
      else Err"
 
   wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,nat,nat,p_count,exception_table,p_count] 
-               => state_type option err"  
+               \<Rightarrow> state_type option err"  
   "wtl_cert i G rT s cert maxs maxr max_pc et pc ==
      case cert!pc of
-        None    => wtl_inst i G rT s cert maxs maxr max_pc et pc
-      | Some s' => if G \<turnstile> s <=' (Some s') then 
+        None    \<Rightarrow> wtl_inst i G rT s cert maxs maxr max_pc et pc
+      | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then 
                     wtl_inst i G rT (Some s') cert maxs maxr max_pc et pc 
                   else Err"
 
 consts 
   wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,nat,nat,p_count,exception_table,p_count,
-                     state_type option] => state_type option err"
+                     state_type option] \<Rightarrow> state_type option err"
 primrec
   "wtl_inst_list []     G rT cert maxs maxr max_pc et pc s = OK s"
   "wtl_inst_list (i#is) G rT cert maxs maxr max_pc et pc s = 
@@ -64,7 +64,7 @@
               
 
 constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] => bool"  
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,nat,exception_table,instr list,certificate] \<Rightarrow> bool"  
  "wtl_method G C pTs rT mxs mxl et ins cert ==  
 	let max_pc = length ins  
   in 
@@ -72,7 +72,7 @@
   wtl_inst_list ins G rT cert mxs mxl max_pc et 0 
                 (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
 
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" 
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool" 
  "wtl_jvm_prog G cert ==  
   wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b,et). wtl_method G C (snd sig) rT maxs maxl et b (cert C sig)) G"
 
@@ -84,12 +84,12 @@
   by simp
 
 lemma merge_def:
-  "!!x. merge G pc mxs mxr max_pc cert ss x = 
+  "\<And>x. merge G pc mxs mxr max_pc cert ss x = 
   (if \<forall>(pc',s') \<in> set ss. pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> s' <=' cert!pc') then
     map (OK \<circ> snd) [(p',t') \<in> ss. p'=pc+1] ++_(sup G mxs mxr) x
-  else Err)" (is "!!x. ?merge ss x = ?if ss x" is "!!x. ?P ss x")
+  else Err)" (is "\<And>x. ?merge ss x = ?if ss x" is "\<And>x. ?P ss x")
 proof (induct ss)
-  show "!!x. ?P [] x" by simp
+  show "\<And>x. ?P [] x" by simp
 next
   have OK_snd: "(\<lambda>u. OK (snd u)) = OK \<circ> snd" by (rule ext) auto
   fix x ss and s::"nat \<times> (state_type option)"
@@ -173,7 +173,7 @@
 qed
 
 lemma wtl_take:
-  "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' ==>
+  "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s'' \<Longrightarrow>
    \<exists>s'. wtl_inst_list (take pc' is) G rT cert mxs mxr mpc et pc s = OK s'"
 proof -
   assume "wtl_inst_list is G rT cert mxs mxr mpc et pc s = OK s''"
@@ -183,7 +183,7 @@
 qed
 
 lemma take_Suc:
-  "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
 proof (induct l)
   show "?P []" by simp
 next
@@ -197,9 +197,9 @@
 qed
 
 lemma wtl_Suc:
- "[| wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'; 
+ "\<lbrakk> wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'; 
      wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s'';
-     Suc pc < length is |] ==>
+     Suc pc < length is \<rbrakk> \<Longrightarrow>
   wtl_inst_list (take (Suc pc) is) G rT cert maxs maxr (length is) et 0 s = OK s''" 
 proof -
   assume "wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s'"
@@ -210,8 +210,8 @@
 qed
 
 lemma wtl_all:
-  "[| wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
-      pc < length is |] ==> 
+  "\<lbrakk> wtl_inst_list is G rT cert maxs maxr (length is) et 0 s \<noteq> Err;
+      pc < length is \<rbrakk> \<Longrightarrow> 
    \<exists>s' s''. wtl_inst_list (take pc is) G rT cert maxs maxr (length is) et 0 s = OK s' \<and> 
             wtl_cert (is!pc) G rT s' cert maxs maxr (length is) et pc = OK s''"
 proof -
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Listn.thy
--- a/src/HOL/MicroJava/BV/Listn.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Listn.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -12,41 +12,41 @@
 
 constdefs
 
- list :: "nat => 'a set => 'a list set"
+ list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
 "list n A == {xs. length xs = n & set xs <= A}"
 
- le :: "'a ord => ('a list)ord"
+ le :: "'a ord \<Rightarrow> ('a list)ord"
 "le r == list_all2 (%x y. x <=_r y)"
 
-syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool"
+syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
        ("(_ /<=[_] _)" [50, 0, 51] 50)
-syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool"
+syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
        ("(_ /<[_] _)" [50, 0, 51] 50)
 translations
  "x <=[r] y" == "x <=_(Listn.le r) y"
  "x <[r] y"  == "x <_(Listn.le r) y"
 
 constdefs
- map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
+ map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
 "map2 f == (%xs ys. map (split f) (zip xs ys))"
 
-syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"
+syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
        ("(_ /+[_] _)" [65, 0, 66] 65)
 translations  "x +[f] y" == "x +_(map2 f) y"
 
-consts coalesce :: "'a err list => 'a list err"
+consts coalesce :: "'a err list \<Rightarrow> 'a list err"
 primrec
 "coalesce [] = OK[]"
 "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
 
 constdefs
- sl :: "nat => 'a sl => 'a list sl"
+ sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
 "sl n == %(A,r,f). (list n A, le r, map2 f)"
 
- sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err"
+ sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
 "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
 
- upto_esl :: "nat => 'a esl => 'a list esl"
+ upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
 "upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
 
 lemmas [simp] = set_update_subsetI
@@ -75,7 +75,7 @@
 done
 
 lemma Cons_less_Conss [simp]:
-  "order r ==> 
+  "order r \<Longrightarrow> 
   x#xs <_(Listn.le r) y#ys = 
   (x <_r y & xs <=[r] ys  |  x = y & xs <_(Listn.le r) ys)"
 apply (unfold lesssub_def)
@@ -83,7 +83,7 @@
 done  
 
 lemma list_update_le_cong:
-  "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
+  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
 apply (unfold unfold_lesub_list)
 apply (unfold Listn.le_def)
 apply (simp add: list_all2_conv_all_nth nth_list_update)
@@ -91,19 +91,19 @@
 
 
 lemma le_listD:
-  "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"
+  "\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p"
 apply (unfold Listn.le_def lesub_def)
 apply (simp add: list_all2_conv_all_nth)
 done
 
 lemma le_list_refl:
-  "!x. x <=_r x ==> xs <=[r] xs"
+  "!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 done
 
 lemma le_list_trans:
-  "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"
+  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 apply clarify
@@ -112,7 +112,7 @@
 done
 
 lemma le_list_antisym:
-  "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"
+  "\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 apply (rule nth_equalityI)
@@ -123,7 +123,7 @@
 done
 
 lemma order_listI [simp, intro!]:
-  "order r ==> order(Listn.le r)"
+  "order r \<Longrightarrow> order(Listn.le r)"
 apply (subst order_def)
 apply (blast intro: le_list_refl le_list_trans le_list_antisym
              dest: order_refl)
@@ -131,35 +131,35 @@
 
 
 lemma lesub_list_impl_same_size [simp]:
-  "xs <=[r] ys ==> size ys = size xs"  
+  "xs <=[r] ys \<Longrightarrow> size ys = size xs"  
 apply (unfold Listn.le_def lesub_def)
 apply (simp add: list_all2_conv_all_nth)
 done 
 
 lemma lesssub_list_impl_same_size:
-  "xs <_(Listn.le r) ys ==> size ys = size xs"
+  "xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs"
 apply (unfold lesssub_def)
 apply auto
 done  
 
 lemma listI:
-  "[| length xs = n; set xs <= A |] ==> xs : list n A"
+  "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
 apply (unfold list_def)
 apply blast
 done
 
 lemma listE_length [simp]:
-   "xs : list n A ==> length xs = n"
+   "xs : list n A \<Longrightarrow> length xs = n"
 apply (unfold list_def)
 apply blast
 done 
 
 lemma less_lengthI:
-  "[| xs : list n A; p < n |] ==> p < length xs"
+  "\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
   by simp
 
 lemma listE_set [simp]:
-  "xs : list n A ==> set xs <= A"
+  "xs : list n A \<Longrightarrow> set xs <= A"
 apply (unfold list_def)
 apply blast
 done 
@@ -183,7 +183,7 @@
 done 
 
 lemma list_not_empty:
-  "? a. a:A ==> ? xs. xs : list n A";
+  "? a. a:A \<Longrightarrow> ? xs. xs : list n A";
 apply (induct "n")
  apply simp
 apply (simp add: in_list_Suc_iff)
@@ -192,18 +192,18 @@
 
 
 lemma nth_in [rule_format, simp]:
-  "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"
+  "!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
 apply (induct "xs")
  apply simp
 apply (simp add: nth_Cons split: nat.split)
 done
 
 lemma listE_nth_in:
-  "[| xs : list n A; i < n |] ==> (xs!i) : A"
+  "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
   by auto
 
 lemma listt_update_in_list [simp, intro!]:
-  "[| xs : list n A; x:A |] ==> xs[i := x] : list n A"
+  "\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
 apply (unfold list_def)
 apply simp
 done 
@@ -215,7 +215,7 @@
 done 
 
 lemma plus_list_Cons [simp]:
-  "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"
+  "(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))"
   by (simp add: plussub_def map2_def split: list.split)
 
 lemma length_plus_list [rule_format, simp]:
@@ -227,7 +227,7 @@
 done
 
 lemma nth_plus_list [rule_format, simp]:
-  "!xs ys i. length xs = n --> length ys = n --> i<n --> 
+  "!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> 
   (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
 apply (induct n)
  apply simp
@@ -239,30 +239,30 @@
 
 
 lemma plus_list_ub1 [rule_format]:
-  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] 
-  ==> xs <=[r] xs +[f] ys"
+  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
+  \<Longrightarrow> xs <=[r] xs +[f] ys"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 done
 
 lemma plus_list_ub2:
-  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
-  ==> ys <=[r] xs +[f] ys"
+  "\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
+  \<Longrightarrow> ys <=[r] xs +[f] ys"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 done 
 
 lemma plus_list_lub [rule_format]:
-  "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A 
-  --> size xs = n & size ys = n --> 
-  xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"
+  "semilat(A,r,f) \<Longrightarrow> !xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
+  \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
+  xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 done 
 
 lemma list_update_incr [rule_format]:
-  "[| semilat(A,r,f); x:A |] ==> set xs <= A --> 
-  (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"
+  "\<lbrakk> semilat(A,r,f); x:A \<rbrakk> \<Longrightarrow> set xs <= A \<longrightarrow> 
+  (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
 apply (unfold unfold_lesub_list)
 apply (simp add: Listn.le_def list_all2_conv_all_nth)
 apply (induct xs)
@@ -273,7 +273,7 @@
 done 
 
 lemma acc_le_listI [intro!]:
-  "[| order r; acc r |] ==> acc(Listn.le r)"
+  "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
 apply (unfold acc_def)
 apply (subgoal_tac
  "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
@@ -323,7 +323,7 @@
 done 
 
 lemma closed_listI:
-  "closed S f ==> closed (list n S) (map2 f)"
+  "closed S f \<Longrightarrow> closed (list n S) (map2 f)"
 apply (unfold closed_def)
 apply (induct n)
  apply simp
@@ -335,7 +335,7 @@
 
 
 lemma semilat_Listn_sl:
-  "!!L. semilat L ==> semilat (Listn.sl n L)"
+  "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
 apply (unfold Listn.sl_def)
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply (simp (no_asm) only: semilat_Def split_conv)
@@ -349,7 +349,7 @@
 
 
 lemma coalesce_in_err_list [rule_format]:
-  "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"
+  "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
 apply (induct n)
  apply simp
 apply clarify
@@ -359,13 +359,13 @@
 apply force
 done 
 
-lemma lem: "!!x xs. x +_(op #) xs = x#xs"
+lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"
   by (simp add: plussub_def)
 
 lemma coalesce_eq_OK1_D [rule_format]:
-  "semilat(err A, Err.le r, lift2 f) ==> 
-  !xs. xs : list n A --> (!ys. ys : list n A --> 
-  (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"
+  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
+  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
+  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
 apply (induct n)
   apply simp
 apply clarify
@@ -376,9 +376,9 @@
 done
 
 lemma coalesce_eq_OK2_D [rule_format]:
-  "semilat(err A, Err.le r, lift2 f) ==> 
-  !xs. xs : list n A --> (!ys. ys : list n A --> 
-  (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"
+  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
+  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
+  (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
 apply (induct n)
  apply simp
 apply clarify
@@ -389,8 +389,8 @@
 done 
 
 lemma lift2_le_ub:
-  "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
-      u:A; x <=_r u; y <=_r u |] ==> z <=_r u"
+  "\<lbrakk> semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
+      u:A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
 apply (unfold semilat_Def plussub_def err_def)
 apply (simp add: lift2_def)
 apply clarify
@@ -401,10 +401,10 @@
 done 
 
 lemma coalesce_eq_OK_ub_D [rule_format]:
-  "semilat(err A, Err.le r, lift2 f) ==> 
-  !xs. xs : list n A --> (!ys. ys : list n A --> 
+  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
+  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us 
-           & us : list n A --> zs <=[r] us))"
+           & us : list n A \<longrightarrow> zs <=[r] us))"
 apply (induct n)
  apply simp
 apply clarify
@@ -418,15 +418,15 @@
 done 
 
 lemma lift2_eq_ErrD:
-  "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] 
-  ==> ~(? u:A. x <=_r u & y <=_r u)"
+  "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A \<rbrakk> 
+  \<Longrightarrow> ~(? u:A. x <=_r u & y <=_r u)"
   by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
 
 
 lemma coalesce_eq_Err_D [rule_format]:
-  "[| semilat(err A, Err.le r, lift2 f) |] 
-  ==> !xs. xs:list n A --> (!ys. ys:list n A --> 
-      coalesce (xs +[f] ys) = Err --> 
+  "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> 
+  \<Longrightarrow> !xs. xs:list n A \<longrightarrow> (!ys. ys:list n A \<longrightarrow> 
+      coalesce (xs +[f] ys) = Err \<longrightarrow> 
       ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
 apply (induct n)
  apply simp
@@ -445,8 +445,8 @@
 done 
 
 lemma closed_map2_list [rule_format]:
-  "closed (err A) (lift2 f) ==> 
-  !xs. xs : list n A --> (!ys. ys : list n A --> 
+  "closed (err A) (lift2 f) \<Longrightarrow> 
+  !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   map2 f xs ys : list n (err A))"
 apply (unfold map2_def)
 apply (induct n)
@@ -458,14 +458,14 @@
 done 
 
 lemma closed_lift2_sup:
-  "closed (err A) (lift2 f) ==> 
+  "closed (err A) (lift2 f) \<Longrightarrow> 
   closed (err (list n A)) (lift2 (sup f))"
   by (fastsimp  simp add: closed_def plussub_def sup_def lift2_def
                           coalesce_in_err_list closed_map2_list
                 split: err.split)
 
 lemma err_semilat_sup:
-  "err_semilat (A,r,f) ==> 
+  "err_semilat (A,r,f) \<Longrightarrow> 
   err_semilat (list n A, Listn.le r, sup f)"
 apply (unfold Err.sl_def)
 apply (simp only: split_conv)
@@ -480,7 +480,7 @@
 done 
 
 lemma err_semilat_upto_esl:
-  "!!L. err_semilat L ==> err_semilat(upto_esl m L)"
+  "\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
 apply (unfold Listn.upto_esl_def)
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply simp
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Opt.thy
--- a/src/HOL/MicroJava/BV/Opt.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Opt.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -11,49 +11,49 @@
 theory Opt = Err:
 
 constdefs
- le :: "'a ord => 'a option ord"
-"le r o1 o2 == case o2 of None => o1=None |
-                              Some y => (case o1 of None => True
-                                                  | Some x => x <=_r y)"
+ le :: "'a ord \<Rightarrow> 'a option ord"
+"le r o1 o2 == case o2 of None \<Rightarrow> o1=None |
+                              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True
+                                                  | Some x \<Rightarrow> x <=_r y)"
 
- opt :: "'a set => 'a option set"
+ opt :: "'a set \<Rightarrow> 'a option set"
 "opt A == insert None {x . ? y:A. x = Some y}"
 
- sup :: "'a ebinop => 'a option ebinop"
+ sup :: "'a ebinop \<Rightarrow> 'a option ebinop"
 "sup f o1 o2 ==  
- case o1 of None => OK o2 | Some x => (case o2 of None => OK o1
-     | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"
+ case o1 of None \<Rightarrow> OK o2 | Some x \<Rightarrow> (case o2 of None \<Rightarrow> OK o1
+     | Some y \<Rightarrow> (case f x y of Err \<Rightarrow> Err | OK z \<Rightarrow> OK (Some z)))"
 
- esl :: "'a esl => 'a option esl"
+ esl :: "'a esl \<Rightarrow> 'a option esl"
 "esl == %(A,r,f). (opt A, le r, sup f)"
 
 lemma unfold_le_opt:
   "o1 <=_(le r) o2 = 
-  (case o2 of None => o1=None | 
-              Some y => (case o1 of None => True | Some x => x <=_r y))"
+  (case o2 of None \<Rightarrow> o1=None | 
+              Some y \<Rightarrow> (case o1 of None \<Rightarrow> True | Some x \<Rightarrow> x <=_r y))"
 apply (unfold lesub_def le_def)
 apply (rule refl)
 done
 
 lemma le_opt_refl:
-  "order r ==> o1 <=_(le r) o1"
+  "order r \<Longrightarrow> o1 <=_(le r) o1"
 by (simp add: unfold_le_opt split: option.split)
 
 lemma le_opt_trans [rule_format]:
-  "order r ==> 
-   o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> o1 <=_(le r) o3"
+  "order r \<Longrightarrow> 
+   o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o3 \<longrightarrow> o1 <=_(le r) o3"
 apply (simp add: unfold_le_opt split: option.split)
 apply (blast intro: order_trans)
 done
 
 lemma le_opt_antisym [rule_format]:
-  "order r ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> o1=o2"
+  "order r \<Longrightarrow> o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o1 \<longrightarrow> o1=o2"
 apply (simp add: unfold_le_opt split: option.split)
 apply (blast intro: order_antisym)
 done
 
 lemma order_le_opt [intro!,simp]:
-  "order r ==> order(le r)"
+  "order r \<Longrightarrow> order(le r)"
 apply (subst order_def)
 apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
 done 
@@ -102,7 +102,7 @@
 
 
 lemma semilat_opt:
-  "!!L. err_semilat L ==> err_semilat (Opt.esl L)"
+  "\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
 proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
   
   fix A r f
@@ -141,11 +141,11 @@
       assume ab: "x = OK a" "y = OK b"
       
       with x 
-      have a: "!!c. a = Some c ==> c : A"
+      have a: "\<And>c. a = Some c \<Longrightarrow> c : A"
         by (clarsimp simp add: opt_def)
 
       from ab y
-      have b: "!!d. b = Some d ==> d : A"
+      have b: "\<And>d. b = Some d \<Longrightarrow> d : A"
         by (clarsimp simp add: opt_def)
       
       { fix c d assume "a = Some c" "b = Some d"
@@ -225,10 +225,10 @@
         obtain "OK d:err A" "OK e:err A" "OK g:err A"
           by simp
         with lub
-        have "[| (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) |]
-          ==> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
+        have "\<lbrakk> (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) \<rbrakk>
+          \<Longrightarrow> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
           by blast
-        hence "[| d <=_r g; e <=_r g |] ==> \<exists>y. d +_f e = OK y \<and> y <=_r g"
+        hence "\<lbrakk> d <=_r g; e <=_r g \<rbrakk> \<Longrightarrow> \<exists>y. d +_f e = OK y \<and> y <=_r g"
           by simp
 
         with ok some xyz xz yz
@@ -263,14 +263,14 @@
 done 
 
 lemma Top_le_conv:
-  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
+  "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
 apply (unfold top_def)
 apply (blast intro: order_antisym)
 done 
 
 
 lemma acc_le_optI [intro!]:
-  "acc r ==> acc(le r)"
+  "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
 apply (simp add: wf_eq_minimal split: option.split)
 apply clarify
@@ -283,8 +283,8 @@
 done 
 
 lemma option_map_in_optionI:
-  "[| ox : opt S; !x:S. ox = Some x --> f x : S |] 
-  ==> option_map f ox : opt S";
+  "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
+  \<Longrightarrow> option_map f ox : opt S";
 apply (unfold option_map_def)
 apply (simp split: option.split)
 apply blast
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Product.thy
--- a/src/HOL/MicroJava/BV/Product.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -11,16 +11,16 @@
 theory Product = Err:
 
 constdefs
- le :: "'a ord => 'b ord => ('a * 'b) ord"
+ le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
 "le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
 
- sup :: "'a ebinop => 'b ebinop => ('a * 'b)ebinop"
+ sup :: "'a ebinop \<Rightarrow> 'b ebinop \<Rightarrow> ('a * 'b)ebinop"
 "sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
 
- esl :: "'a esl => 'b esl => ('a * 'b ) esl"
+ esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
 "esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
 
-syntax "@lesubprod" :: "'a*'b => 'a ord => 'b ord => 'b => bool"
+syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
        ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
 translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
 
@@ -49,7 +49,7 @@
 
 
 lemma acc_le_prodI [intro!]:
-  "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"
+  "\<lbrakk> acc rA; acc rB \<rbrakk> \<Longrightarrow> acc(Product.le rA rB)"
 apply (unfold acc_def)
 apply (rule wf_subset)
  apply (erule wf_lex_prod)
@@ -59,7 +59,7 @@
 
 
 lemma closed_lift2_sup:
-  "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==> 
+  "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> 
   closed (err(A<*>B)) (lift2(sup f g))";
 apply (unfold closed_def plussub_def lift2_def err_def sup_def)
 apply (simp split: err.split)
@@ -72,12 +72,12 @@
 
 
 lemma plus_eq_Err_conv [simp]:
-  "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |] 
-  ==> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+  "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk> 
+  \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
 proof -
   have plus_le_conv2:
-    "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
-                 OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
+    "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
+                 OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
     by (rule plus_le_conv [THEN iffD1])
   case rule_context
   thus ?thesis
@@ -110,7 +110,7 @@
 qed
 
 lemma err_semilat_Product_esl:
-  "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"
+  "\<And>L1 L2. \<lbrakk> err_semilat L1; err_semilat L2 \<rbrakk> \<Longrightarrow> err_semilat(Product.esl L1 L2)"
 apply (unfold esl_def Err.sl_def)
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply simp
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -13,134 +13,134 @@
 
 theory Semilat = While_Combinator:
 
-types 'a ord    = "'a => 'a => bool"
-      'a binop  = "'a => 'a => 'a"
+types 'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
+      'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
       'a sl     = "'a set * 'a ord * 'a binop"
 
 consts
- "@lesub"   :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
- "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
+ "@lesub"   :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
+ "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
 defs
 lesub_def:   "x <=_r y == r x y"
 lesssub_def: "x <_r y  == x <=_r y & x ~= y"
 
 consts
- "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
+ "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
 defs
 plussub_def: "x +_f y == f x y"
 
 
 constdefs
- ord :: "('a*'a)set => 'a ord"
+ ord :: "('a*'a)set \<Rightarrow> 'a ord"
 "ord r == %x y. (x,y):r"
 
- order :: "'a ord => bool"
+ order :: "'a ord \<Rightarrow> bool"
 "order r == (!x. x <=_r x) &
-            (!x y. x <=_r y & y <=_r x --> x=y) &
-            (!x y z. x <=_r y & y <=_r z --> x <=_r z)"
+            (!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) &
+            (!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)"
 
- acc :: "'a ord => bool"
+ acc :: "'a ord \<Rightarrow> bool"
 "acc r == wf{(y,x) . x <_r y}"
 
- top :: "'a ord => 'a => bool"
+ top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
 "top r T == !x. x <=_r T"
 
- closed :: "'a set => 'a binop => bool"
+ closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool"
 "closed A f == !x:A. !y:A. x +_f y : A"
 
- semilat :: "'a sl => bool"
+ semilat :: "'a sl \<Rightarrow> bool"
 "semilat == %(A,r,f). order r & closed A f &
                 (!x:A. !y:A. x <=_r x +_f y)  &
                 (!x:A. !y:A. y <=_r x +_f y)  &
-                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
 
- is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
+ is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 "is_ub r x y u == (x,u):r & (y,u):r"
 
- is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
-"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+ is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
 
- some_lub :: "('a*'a)set => 'a => 'a => 'a"
+ some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 "some_lub r x y == SOME z. is_lub r x y z"
 
 
 lemma order_refl [simp, intro]:
-  "order r ==> x <=_r x";
+  "order r \<Longrightarrow> x <=_r x";
   by (simp add: order_def)
 
 lemma order_antisym:
-  "[| order r; x <=_r y; y <=_r x |] ==> x = y"
+  "\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
 apply (unfold order_def)
 apply (simp (no_asm_simp))  
 done
 
 lemma order_trans:
-   "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"
+   "\<lbrakk> order r; x <=_r y; y <=_r z \<rbrakk> \<Longrightarrow> x <=_r z"
 apply (unfold order_def)
 apply blast
 done 
 
 lemma order_less_irrefl [intro, simp]:
-   "order r ==> ~ x <_r x"
+   "order r \<Longrightarrow> ~ x <_r x"
 apply (unfold order_def lesssub_def)
 apply blast
 done 
 
 lemma order_less_trans:
-  "[| order r; x <_r y; y <_r z |] ==> x <_r z"
+  "\<lbrakk> order r; x <_r y; y <_r z \<rbrakk> \<Longrightarrow> x <_r z"
 apply (unfold order_def lesssub_def)
 apply blast
 done 
 
 lemma topD [simp, intro]:
-  "top r T ==> x <=_r T"
+  "top r T \<Longrightarrow> x <=_r T"
   by (simp add: top_def)
 
 lemma top_le_conv [simp]:
-  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
+  "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
   by (blast intro: order_antisym)
 
 lemma semilat_Def:
 "semilat(A,r,f) == order r & closed A f & 
                  (!x:A. !y:A. x <=_r x +_f y) & 
                  (!x:A. !y:A. y <=_r x +_f y) & 
-                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
 apply (unfold semilat_def split_conv [THEN eq_reflection])
 apply (rule refl [THEN eq_reflection])
 done
 
 lemma semilatDorderI [simp, intro]:
-  "semilat(A,r,f) ==> order r"
+  "semilat(A,r,f) \<Longrightarrow> order r"
   by (simp add: semilat_Def)
 
 lemma semilatDclosedI [simp, intro]:
-  "semilat(A,r,f) ==> closed A f"
+  "semilat(A,r,f) \<Longrightarrow> closed A f"
 apply (unfold semilat_Def)
 apply simp
 done
 
 lemma semilat_ub1 [simp]:
-  "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"
+  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
   by (unfold semilat_Def, simp)
 
 lemma semilat_ub2 [simp]:
-  "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"
+  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
   by (unfold semilat_Def, simp)
 
 lemma semilat_lub [simp]:
- "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
+ "\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
   by (unfold semilat_Def, simp)
 
 
 lemma plus_le_conv [simp]:
-  "[| x:A; y:A; z:A; semilat(A,r,f) |] 
-  ==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
+  "\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk> 
+  \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
 apply (unfold semilat_Def)
 apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
 done
 
 lemma le_iff_plus_unchanged:
-  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)"
+  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
 apply (rule iffI)
  apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
 apply (erule subst)
@@ -148,7 +148,7 @@
 done 
 
 lemma le_iff_plus_unchanged2:
-  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)"
+  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
 apply (rule iffI)
  apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
 apply (erule subst)
@@ -157,7 +157,7 @@
 
 
 lemma closedD:
-  "[| closed A f; x:A; y:A |] ==> x +_f y : A"
+  "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
 apply (unfold closed_def)
 apply blast
 done 
@@ -167,15 +167,15 @@
 
 
 lemma is_lubD:
-  "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+  "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
   by (simp add: is_lub_def)
 
 lemma is_ubI:
-  "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"
+  "\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u"
   by (simp add: is_ub_def)
 
 lemma is_ubD:
-  "is_ub r x y u ==> (x,u) : r & (y,u) : r"
+  "is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r"
   by (simp add: is_ub_def)
 
 
@@ -192,8 +192,8 @@
 done
 
 lemma extend_lub:
-  "[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |] 
-  ==> EX v. is_lub (r^* ) x' y v"
+  "\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk> 
+  \<Longrightarrow> EX v. is_lub (r^* ) x' y v"
 apply (unfold is_lub_def is_ub_def)
 apply (case_tac "(y,x) : r^*")
  apply (case_tac "(y,x') : r^*")
@@ -207,7 +207,7 @@
 done
 
 lemma single_valued_has_lubs [rule_format]:
-  "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> 
+  "\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow> 
   (EX z. is_lub (r^* ) x y z))"
 apply (erule converse_rtrancl_induct)
  apply clarify
@@ -218,7 +218,7 @@
 done
 
 lemma some_lub_conv:
-  "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u"
+  "\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u"
 apply (unfold some_lub_def is_lub_def)
 apply (rule someI2)
  apply assumption
@@ -226,8 +226,8 @@
 done
 
 lemma is_lub_some_lub:
-  "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] 
-  ==> is_lub (r^* ) x y (some_lub (r^* ) x y)";
+  "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk> 
+  \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
   by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)
 
 subsection{*An executable lub-finder*}
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Typing_Framework.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -15,23 +15,23 @@
   's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
 
 constdefs
- bounded :: "'s step_type => nat => bool"
+ bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
 "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
 
- stable :: "'s ord => 's step_type => 's list => nat => bool"
+ stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
 "stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
 
- stables :: "'s ord => 's step_type => 's list => bool"
+ stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
 "stables r step ss == !p<size ss. stable r step ss p"
 
- is_bcv :: "'s ord => 's => 's step_type 
-           => nat => 's set => ('s list => 's list) => bool"  
+ is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type 
+           \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"  
 "is_bcv r T step n A bcv == !ss : list n A.
    (!p<n. (bcv ss)!p ~= T) =
    (? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
 
  wt_step ::
-"'s ord => 's => 's step_type => 's list => bool"
+"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
 "wt_step r T step ts ==
  !p<size(ts). ts!p ~= T & stable r step ts p"
 
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -11,10 +11,10 @@
 
 constdefs
 
-dynamic_wt :: "'s ord => 's err step_type => 's err list => bool"
+dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
 "dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
 
-static_wt :: "'s ord => (nat => 's => bool) => 's step_type => 's list => bool"
+static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
 "static_wt r app step ts == 
   \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
 
@@ -28,14 +28,14 @@
 "err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow> 
   if app p t' then map_snd OK (step p t') else map_err (step p t')"
 
-non_empty :: "'s step_type => bool"
+non_empty :: "'s step_type \<Rightarrow> bool"
 "non_empty step == \<forall>p t. step p t \<noteq> []"
 
 
 lemmas err_step_defs = err_step_def map_snd_def map_err_def
 
 lemma non_emptyD:
-  "non_empty step ==> \<exists>q t'. (q,t') \<in> set(step p t)"
+  "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
 proof (unfold non_empty_def)
   assume "\<forall>p t. step p t \<noteq> []"
   hence "step p t \<noteq> []" by blast
@@ -47,9 +47,9 @@
 
 
 lemma dynamic_imp_static:
-  "[| bounded step (size ts); non_empty step;
-      dynamic_wt r (err_step app step) ts |] 
-  ==> static_wt r app step (map ok_val ts)"
+  "\<lbrakk> bounded step (size ts); non_empty step;
+      dynamic_wt r (err_step app step) ts \<rbrakk> 
+  \<Longrightarrow> static_wt r app step (map ok_val ts)"
 proof (unfold static_wt_def, intro strip, rule conjI)
 
   assume b:  "bounded step (size ts)"
@@ -112,8 +112,8 @@
 
 
 lemma static_imp_dynamic:
-  "[| static_wt r app step ts; bounded step (size ts) |] 
-  ==> dynamic_wt r (err_step app step) (map OK ts)"
+  "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk> 
+  \<Longrightarrow> dynamic_wt r (err_step app step) (map OK ts)"
 proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
   assume bounded: "bounded step (size ts)"
   assume static:  "static_wt r app step ts"
diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -34,6 +34,6 @@
 
 syntax (xsymbols)
   exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
-              ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
+              ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60)
 
 end