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"