# HG changeset patch
# User kleing
# Date 969525769 -7200
# Node ID 7164dc0d24d8a3d57f8cf6115b511ce5a0e67526
# Parent  30693ebd16aee2f1644dd1a426f8d76b8e5a6b60
unsymbolized

diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -11,53 +11,53 @@
 
 types
  method_type = "state_type option list"
- class_type	 = "sig \<Rightarrow> method_type"
- prog_type	 = "cname \<Rightarrow> class_type"
+ class_type	 = "sig => method_type"
+ prog_type	 = "cname => class_type"
 
 constdefs
-wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \<Rightarrow> bool"
-"wt_instr i G rT phi max_pc pc \<equiv> 
+wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool"
+"wt_instr i G rT phi max_pc pc == 
     app i G rT (phi!pc) \<and>
    (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
 
-wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
-"wt_start G C pTs mxl phi \<equiv> 
+wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => 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,instr list,method_type] \<Rightarrow> bool"
-"wt_method G C pTs rT mxl ins phi \<equiv>
+wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool"
+"wt_method G C pTs rT mxl ins phi ==
 	let max_pc = length ins
         in
 	0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
-	(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
+	(\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi max_pc pc)"
 
-wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
-"wt_jvm_prog G phi \<equiv>
+wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
+"wt_jvm_prog G phi ==
    wf_prog (\<lambda>G C (sig,rT,maxl,b).
               wt_method G C (snd sig) rT maxl b (phi C sig)) G"
 
 
 
 lemma wt_jvm_progD:
-"wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
+"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
 by (unfold wt_jvm_prog_def, blast)
 
 lemma wt_jvm_prog_impl_wt_instr:
-"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \<rbrakk> 
- \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
+"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins |] 
+ ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
     simp, simp add: wf_mdecl_def wt_method_def)
 
 lemma wt_jvm_prog_impl_wt_start:
-"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \<rbrakk> \<Longrightarrow> 
+"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) |] ==> 
  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 add: wf_mdecl_def wt_method_def)
 
 (* for most instructions wt_instr collapses: *)
 lemma  
-"succs i pc = [pc+1] \<Longrightarrow> wt_instr i G rT phi max_pc pc = 
+"succs i pc = [pc+1] ==> wt_instr i G rT phi max_pc pc = 
  (app i G rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
 by (simp add: wt_instr_def) 
 
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -24,13 +24,13 @@
 done
 
 lemma Load_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
    method (G,C) sig = Some (C,rT,maxl,ins); 
    ins!pc = Load idx; 
    wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (rule approx_loc_imp_approx_val_sup)
@@ -39,13 +39,13 @@
 done
 
 lemma Store_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins);
   ins!pc = Store idx;
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (blast intro: approx_stk_imp_approx_stk_sup)
@@ -54,18 +54,18 @@
 
 
 lemma conf_Intg_Integer [iff]:
-  "G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
+  "G,h \<turnstile> Intg i ::\<preceq> PrimT Integer"
 by (simp add: conf_def)
 
 
 lemma Bipush_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins!pc = Bipush i; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk>
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |]
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
 done
@@ -73,7 +73,7 @@
 lemma NT_subtype_conv:
   "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
 proof -
-  have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))"
+  have "!!T T'. G \<turnstile> T' \<preceq> T ==> T' = NT --> (T=NT | (\<exists>C. T = Class C))"
     apply (erule widen.induct)
     apply auto
     apply (case_tac R)
@@ -86,13 +86,13 @@
 qed
 
 lemma Aconst_null_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins!pc =  Aconst_null; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (force simp add: approx_val_Null NT_subtype_conv)
@@ -101,8 +101,8 @@
 
 
 lemma Cast_conf2:
-  "\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<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\<Colon>\<preceq>T"
+  "[|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"
 apply (unfold cast_ok_def)
 apply (frule widen_Class)
 apply (elim exE disjE)
@@ -114,26 +114,26 @@
 
 
 lemma Checkcast_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins!pc = Checkcast D; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
 done
 
 
 lemma Getfield_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins!pc = Getfield F D; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
 apply (frule conf_widen)
 apply assumption+
@@ -147,13 +147,13 @@
 done
 
 lemma Putfield_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins!pc = Putfield F D; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
 apply (clarsimp simp add: approx_val_def)
 apply (frule conf_widen)
@@ -174,13 +174,13 @@
   by fast
 
 lemma New_correct:
-"\<lbrakk> wf_prog wt G;
+"[| wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins!pc = New cl_idx; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
 		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
        split: option.split)
@@ -199,13 +199,13 @@
 lemmas [simp del] = split_paired_Ex
 
 lemma Invoke_correct:
-"\<lbrakk> wt_jvm_prog G phi; 
+"[| wt_jvm_prog G phi; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Invoke C' mn pTs; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>" 
 proof -
   assume wtprog: "wt_jvm_prog G phi"
   assume method: "method (G,C) sig = Some (C,rT,maxl,ins)"
@@ -282,7 +282,7 @@
     by simp
 
   with state' method ins 
-  have Null_ok: "oX = Null \<Longrightarrow> ?thesis"
+  have Null_ok: "oX = Null ==> ?thesis"
     by (simp add: correct_state_def raise_xcpt_def)
   
   { fix ref
@@ -434,13 +434,13 @@
 lemmas [simp del] = map_append
 
 lemma Return_correct:
-"\<lbrakk> wt_jvm_prog G phi;  
+"[| wt_jvm_prog G phi;  
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Return; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
 apply (frule wt_jvm_prog_impl_wt_instr)
 apply (assumption, erule Suc_lessD)
@@ -455,102 +455,102 @@
 lemmas [simp] = map_append
 
 lemma Goto_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Goto branch; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
 done
 
 
 lemma Ifcmpeq_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Ifcmpeq branch; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
 done
 
 lemma Pop_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Pop;
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
 done
 
 lemma Dup_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Dup;
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
 lemma Dup_x1_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Dup_x1;
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
 lemma Dup_x2_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Dup_x2;
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
 lemma Swap_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Swap;
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
 done
 
 lemma IAdd_correct:
-"\<lbrakk> wf_prog wt G; 
+"[| wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = IAdd; 
   wt_instr (ins!pc) G rT (phi C sig) (length ins) 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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
 done
@@ -559,11 +559,11 @@
 (** instr correct **)
 
 lemma instr_correct:
-"\<lbrakk> wt_jvm_prog G phi; 
+"[| wt_jvm_prog G phi; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   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> \<rbrakk> 
-\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+==> G,phi \<turnstile>JVM state'\<surd>"
 apply (frule wt_jvm_prog_impl_wt_instr_cor)
 apply assumption+
 apply (cases "ins!pc")
@@ -583,13 +583,13 @@
 
 lemma correct_state_impl_Some_method:
   "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
-  \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
+  ==> \<exists>meth. method (G,C) sig = Some(C,meth)"
 by (auto simp add: correct_state_def Let_def)
 
 
 lemma BV_correct_1 [rule_format]:
-"\<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>"
+"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] 
+ ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>"
 apply (simp only: split_tupled_all)
 apply (rename_tac xp hp frs)
 apply (case_tac xp)
@@ -605,12 +605,12 @@
 
 
 lemma L0:
-  "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
+  "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
 by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
 
 lemma L1:
-  "\<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>"
+  "[|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>"
 apply (drule L0)
 apply assumption
 apply (fast intro: BV_correct_1)
@@ -618,7 +618,7 @@
 
 
 theorem BV_correct [rule_format]:
-"\<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>"
+"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>"
 apply (unfold exec_all_def)
 apply (erule rtrancl_induct)
  apply simp
@@ -627,8 +627,8 @@
 
 
 theorem BV_correct_initial:
-"\<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)))"
+"[| 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> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
 apply (drule BV_correct)
 apply assumption+
 apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -19,51 +19,52 @@
 
 
 consts
-  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+  strict  :: "('a => 'b err) => ('a err => 'b err)"
 primrec
   "strict f Err    = Err"
   "strict f (Ok x) = f x"
 
-consts
-  opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
-primrec
-  "opt_map f None     = None"
-  "opt_map f (Some x) = Some (f x)"
 
 consts
-  val :: "'a err \<Rightarrow> 'a"
+  val :: "'a err => 'a"
 primrec
   "val (Ok s) = s"
 
   
 constdefs
   (* lifts a relation to err with Err as top element *)
-  lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
-  "lift_top P a' a \<equiv> case a of 
-                       Err  \<Rightarrow> True
-                     | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
+  lift_top :: "('a => 'b => bool) => ('a err => 'b err => bool)"
+  "lift_top P a' a == case a of 
+                       Err  => True
+                     | Ok t => (case a' of Err => False | Ok t' => P t' t)"
 
   (* lifts a relation to option with None as bottom element *)
-  lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
-  "lift_bottom P a' a \<equiv> case a' of 
-                          None    \<Rightarrow> True 
-                        | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
+  lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
+  "lift_bottom P a' a == case a' of 
+                          None    => True 
+                        | Some t' => (case a of None => False | Some t => P t' t)"
 
-  sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
-  "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ \<turnstile> _ <=o _" [71,71] 70)
+  "sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+
+  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
+              ("_ \<turnstile> _ <=l _"  [71,71] 70)
+  "G \<turnstile> LT <=l LT' == list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
 
-  sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
-             ("_ \<turnstile> _ <=l _"  [71,71] 70)
-  "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
-
-  sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  
+  sup_state :: "['code prog,state_type,state_type] => bool"	  
                ("_ \<turnstile> _ <=s _"  [71,71] 70)
-  "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+  "G \<turnstile> s <=s s' == (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+
+  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
+                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
+  "sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
 
-  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
-                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
-  "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
-
+syntax (HTML output) 
+  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ |- _ <=o _")
+  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" ("_ |- _ <=l _"  [71,71] 70)
+  sup_state :: "['code prog,state_type,state_type] => bool"	("_ |- _ <=s _"  [71,71] 70)
+  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" ("_ |- _ <=' _"  [71,71] 70)
+                   
 
 lemma not_Err_eq [iff]:
   "(x \<noteq> Err) = (\<exists>a. x = Ok a)" 
@@ -223,7 +224,7 @@
   by (simp add: sup_ty_opt_def)
 
 theorem sup_ty_opt_Ok:
-  "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> x. a = Ok x"
+  "G \<turnstile> a <=o (Ok b) ==> \<exists> x. a = Ok x"
   by (clarsimp simp add: sup_ty_opt_def)
 
 lemma widen_PrimT_conv1 [simp]:
@@ -250,10 +251,10 @@
 
 
 theorem sup_loc_length:
-  "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
+  "G \<turnstile> a <=l b ==> length a = length b"
 proof -
   assume G: "G \<turnstile> a <=l b"
-  have "\<forall> b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
+  have "\<forall> b. (G \<turnstile> a <=l b) --> length a = length b"
     by (induct a, auto)
   with G
   show ?thesis by blast
@@ -263,7 +264,7 @@
   "[| G \<turnstile> a <=l b; n < length a |] ==> 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) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
+  have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))"
     (is "?P a")
   proof (induct a)
     show "?P []" by simp
@@ -285,7 +286,7 @@
 
 
 theorem all_nth_sup_loc:
-  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> 
+  "\<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")
 proof (induct a)
   show "?P []" by simp
@@ -295,14 +296,14 @@
   show "?P (l#ls)"
   proof (intro strip)
     fix b
-    assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
+    assume f: "\<forall>n. n < length (l # ls) --> (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 \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
+    have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))"
       by auto
 
     with f b l IH
@@ -318,7 +319,7 @@
 proof -
   assume l: "length a = length b"
 
-  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
+  have "\<forall>b. length a = length b --> (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
@@ -384,7 +385,7 @@
 
 
 theorem sup_loc_update [rule_format]:
-  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
+  "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> 
           (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
 proof (induct x)
   show "?P []" by simp
@@ -427,7 +428,7 @@
   by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
 
 theorem sup_state_ignore_fst:  
-  "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
+  "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)"
   by (simp add: sup_state_def)
 
 theorem sup_state_rev_fst:
@@ -460,15 +461,15 @@
 
 
 theorem sup_ty_opt_trans [trans]:
-  "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
+  "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c"
   by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
 
 theorem sup_loc_trans [trans]:
-  "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
+  "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c"
 proof -
   assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
  
-  hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
+  hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))"
   proof (intro strip)
     fix n 
     assume n: "n < length a"
@@ -490,11 +491,11 @@
   
 
 theorem sup_state_trans [trans]:
-  "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
+  "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c"
   by (auto intro: sup_loc_trans simp add: sup_state_def)
 
 theorem sup_state_opt_trans [trans]:
-  "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
+  "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c"
   by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
 
 
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -11,26 +11,26 @@
 theory Correct = BVSpec:
 
 constdefs
- approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
-"approx_val G h v any \<equiv> case any of Err \<Rightarrow> True | Ok T \<Rightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
+ 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_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
-"approx_loc G hp loc LT \<equiv> list_all2 (approx_val G hp) loc LT"
+ approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
+"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
 
- approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
-"approx_stk G hp stk ST \<equiv> approx_loc G hp stk (map Ok ST)"
+ approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
+"approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
 
- correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
-"correct_frame G hp \<equiv> \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
+ correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => 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"
 
- correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
-"correct_frame_opt G hp s \<equiv> case s of None \<Rightarrow> \<lambda>maxl ins f. False | Some t \<Rightarrow> correct_frame G hp t"
+ correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] => frame => bool"
+"correct_frame_opt G hp s == case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t"
 
 
 consts
- correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
+ correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool"
 primrec
 "correct_frames G hp phi rT0 sig0 [] = True"
 
@@ -52,13 +52,13 @@
 
 
 constdefs
- correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
+ correct_state :: "[jvm_prog,prog_type,jvm_state] => bool"
                   ("_,_\<turnstile>JVM _\<surd>"  [51,51] 50)
-"correct_state G phi \<equiv> \<lambda>(xp,hp,frs).
+"correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
-     None \<Rightarrow> (case frs of
-	           [] \<Rightarrow> True
-             | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and>
+     None => (case frs of
+	           [] => True
+             | (f#fs) => G\<turnstile>h hp\<surd> \<and>
 			(let (stk,loc,C,sig,pc) = f
 		         in
                          \<exists>rT maxl ins s.
@@ -66,11 +66,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 \<Rightarrow> True" 
+   | Some x => True" 
 
 
 lemma sup_heap_newref:
-  "hp x = None \<Longrightarrow> hp \<le>| hp(newref hp \<mapsto> obj)"
+  "hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)"
 apply (unfold hext_def)
 apply clarsimp
 apply (drule newref_None 1) back
@@ -78,7 +78,7 @@
 .
 
 lemma sup_heap_update_value:
-  "hp a = Some (C,od') \<Longrightarrow> hp \<le>| hp (a \<mapsto> (C,od))"
+  "hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))"
 by (simp add: hext_def)
 
 
@@ -93,29 +93,29 @@
 by (auto intro: null simp add: approx_val_def)
 
 lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
-  "wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')"
+  "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' --> approx_val G hp v (Ok T')"
 by (cases T) (auto intro: conf_widen simp add: approx_val_def)
 
 lemma approx_val_imp_approx_val_sup_heap [rule_format]:
-  "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
+  "approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at"
 apply (simp add: approx_val_def split: err.split)
 apply (blast intro: conf_hext)
 .
 
 lemma approx_val_imp_approx_val_heap_update:
-  "\<lbrakk>hp a = Some obj'; G,hp\<turnstile> v\<Colon>\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
-  \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
+  "[|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"
 by (cases v, auto simp add: obj_ty_def conf_def)
 
 lemma approx_val_imp_approx_val_sup [rule_format]:
-  "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
+  "wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') --> (approx_val G h v us')"
 apply (simp add: sup_PTS_eq approx_val_def split: err.split)
 apply (blast intro: conf_widen)
 .
 
 lemma approx_loc_imp_approx_val_sup:
-  "\<lbrakk>wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at\<rbrakk>
-  \<Longrightarrow> approx_val G hp v at"
+  "[|wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at|]
+  ==> approx_val G hp v at"
 apply (unfold approx_loc_def)
 apply (unfold list_all2_def)
 apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
@@ -129,8 +129,8 @@
 by (simp add: approx_loc_def)
 
 lemma assConv_approx_stk_imp_approx_loc [rule_format]:
-  "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
-  \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> 
+  "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
+  --> length tys_n = length ts --> approx_stk G hp s tys_n --> 
   approx_loc G hp s (map Ok ts)"
 apply (unfold approx_stk_def approx_loc_def list_all2_def)
 apply (clarsimp simp add: all_set_conv_all_nth)
@@ -140,7 +140,7 @@
 
 
 lemma approx_loc_imp_approx_loc_sup_heap [rule_format]:
-  "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
+  "\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' --> approx_loc G hp' lvars lt"
 apply (unfold approx_loc_def list_all2_def)
 apply (cases lt)
  apply simp
@@ -150,7 +150,7 @@
 .
 
 lemma approx_loc_imp_approx_loc_sup [rule_format]:
-  "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
+  "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'"
 apply (unfold sup_loc_def approx_loc_def list_all2_def)
 apply (auto simp add: all_set_conv_all_nth)
 apply (auto elim: approx_val_imp_approx_val_sup)
@@ -158,8 +158,8 @@
 
 
 lemma approx_loc_imp_approx_loc_subst [rule_format]:
-  "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) 
-  \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
+  "\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X) 
+  --> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
 apply (unfold approx_loc_def list_all2_def)
 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
 .
@@ -168,7 +168,7 @@
 lemmas [cong] = conj_cong 
 
 lemma approx_loc_append [rule_format]:
-  "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> 
+  "\<forall>L1 l2 L2. length l1=length L1 --> 
   approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
 apply (unfold approx_loc_def list_all2_def)
 apply simp
@@ -192,12 +192,12 @@
 
 
 lemma approx_stk_imp_approx_stk_sup_heap [rule_format]:
-  "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
+  "\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' --> approx_stk G hp' lvars lt"
 by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
 
 lemma approx_stk_imp_approx_stk_sup [rule_format]:
-  "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) 
-  \<longrightarrow> approx_stk G hp lvars st'" 
+  "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st')) 
+  --> approx_stk G hp lvars st'" 
 by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
 
 lemma approx_stk_Nil [iff]:
@@ -215,7 +215,7 @@
 by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
 
 lemma approx_stk_append_lemma:
-  "approx_stk G hp stk (S@ST') \<Longrightarrow>
+  "approx_stk G hp stk (S@ST') ==>
    (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and> 
              approx_stk G hp s S \<and> approx_stk G hp stk' ST')"
 by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
@@ -224,7 +224,7 @@
 (** oconf **)
 
 lemma correct_init_obj:
-  "\<lbrakk>is_class G C; wf_prog wt G\<rbrakk> \<Longrightarrow> 
+  "[|is_class G C; wf_prog wt G|] ==> 
   G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
 apply (unfold oconf_def lconf_def)
 apply (simp add: map_of_map)
@@ -233,13 +233,13 @@
 
 
 lemma oconf_imp_oconf_field_update [rule_format]:
-  "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
-  \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
+  "[|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>"
 by (simp add: oconf_def lconf_def)
 
 
 lemma oconf_imp_oconf_heap_newref [rule_format]:
-"hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
+"hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
 apply (unfold oconf_def lconf_def)
 apply simp
 apply (fast intro: conf_hext sup_heap_newref)
@@ -247,8 +247,8 @@
 
 
 lemma oconf_imp_oconf_heap_update [rule_format]:
-  "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> 
-  \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
+  "hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd> 
+  --> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
 apply (unfold oconf_def lconf_def)
 apply simp
 apply (force intro: approx_val_imp_approx_val_heap_update)
@@ -259,14 +259,14 @@
 
 
 lemma hconf_imp_hconf_newref [rule_format]:
-  "hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
+  "hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
 apply (simp add: hconf_def)
 apply (fast intro: oconf_imp_oconf_heap_newref)
 .
 
 lemma hconf_imp_hconf_field_update [rule_format]:
   "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
-  G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
+  G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
 apply (simp add: hconf_def)
 apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update 
              simp add: obj_ty_def)
@@ -277,10 +277,10 @@
 lemmas [simp del] = fun_upd_apply
 
 lemma correct_frames_imp_correct_frames_field_update [rule_format]:
-  "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> 
-  hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
-  G,hp\<turnstile>v\<Colon>\<preceq>fd 
-  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
+  "\<forall>rT C sig. correct_frames G hp phi rT sig frs --> 
+  hp a = Some (C,od) --> map_of (fields (G, C)) fl = Some fd --> 
+  G,hp\<turnstile>v::\<preceq>fd 
+  --> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
 apply (induct frs)
  apply simp
 apply (clarsimp simp add: correct_frame_def) (*takes long*)
@@ -300,8 +300,8 @@
 .
 
 lemma correct_frames_imp_correct_frames_newref [rule_format]:
-  "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
-  \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
+  "\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
+  --> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
 apply (induct frs)
  apply simp
 apply (clarsimp simp add: correct_frame_def)
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -9,30 +9,30 @@
 theory LBVComplete = BVSpec + LBVSpec + StepMono:
 
 constdefs
-  contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
-  "contains_targets ins cert phi pc \<equiv> 
+  contains_targets :: "[instr list, certificate, method_type, p_count] => bool"
+  "contains_targets ins cert phi pc == 
      \<forall>pc' \<in> set (succs (ins!pc) pc). 
-      pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'"
+      pc' \<noteq> pc+1 \<and> pc' < length ins --> cert!pc' = phi!pc'"
 
-  fits :: "[instr list, certificate, method_type] \<Rightarrow> bool"
-  "fits ins cert phi \<equiv> \<forall>pc. pc < length ins \<longrightarrow> 
+  fits :: "[instr list, certificate, method_type] => bool"
+  "fits ins cert phi == \<forall>pc. pc < length ins --> 
                        contains_targets ins cert phi pc \<and>
                        (cert!pc = None \<or> cert!pc = phi!pc)"
 
-  is_target :: "[instr list, p_count] \<Rightarrow> bool" 
-  "is_target ins pc \<equiv> 
+  is_target :: "[instr list, p_count] => 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] \<Rightarrow> certificate"
-  "make_cert ins phi \<equiv> 
+  make_cert :: "[instr list, method_type] => 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] \<Rightarrow> prog_certificate"
-  "make_Cert G Phi \<equiv>  \<lambda> C sig.
-     let (C,x,y,mdecls)  = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
-         (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
+  make_Cert :: "[jvm_prog, prog_type] => prog_certificate"
+  "make_Cert G Phi ==  \<lambda> C sig.
+     let (C,x,y,mdecls)  = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+         (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
      in make_cert b (Phi C sig)"
   
 
@@ -197,14 +197,14 @@
   have app: "app (ins!pc) G rT (phi!pc)" by (simp add: wt_instr_def)
 
   from wt pc
-  have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
+  have pc': "!!pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
     by (simp add: wt_instr_def)
 
   let ?s' = "step (ins!pc) G (phi!pc)"
 
   from wt fits pc
-  have cert: "!!pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
-    \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
+  have cert: "!!pc'. [|pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1|] 
+    ==> G \<turnstile> ?s' <=' cert!pc'"
     by (auto dest: fitsD simp add: wt_instr_def)     
 
   from app pc cert pc'
@@ -324,14 +324,14 @@
 *}
 
 theorem wt_imp_wtl_inst_list:
-"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> 
-        wt_instr (all_ins ! pc') G rT phi (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> 
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins --> 
+        wt_instr (all_ins ! pc') G rT phi (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)) --> 
              wtl_inst_list ins G rT cert (length all_ins) pc s \<noteq> Err)" 
-(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"  
+(is "\<forall>pc. ?wt --> ?fits --> ?l pc ins --> ?len pc --> ?wtl pc ins"  
  is "\<forall>pc. ?C pc ins" is "?P ins") 
 proof (induct "?P" "ins")
   case Nil
@@ -343,7 +343,7 @@
   show "?P (i#ins')" 
   proof (intro allI impI, elim exE conjE)
     fix pc s l
-    assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
+    assume wt  : "\<forall>pc'. pc' < length all_ins --> 
                         wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
     assume fits: "fits all_ins cert phi"
     assume l   : "pc < length all_ins"
@@ -362,7 +362,7 @@
     from Cons
     have "?C (Suc pc) ins'" by blast
     with wt fits pc
-    have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
+    have IH: "?len (Suc pc) --> ?wtl (Suc pc) ins'" by auto
 
     show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \<noteq> Err" 
     proof (cases "?len (Suc pc)")
@@ -422,20 +422,10 @@
     by (rule fits_imp_wtl_method_complete)
 qed
 
-lemma unique_set:
-"(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> 
-  a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
-  by (induct "l") auto
-
-lemma unique_epsilon:
-  "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> 
-  (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
-  by (auto simp add: unique_set)
-
 
 theorem wtl_complete: 
   "wt_jvm_prog G Phi ==> wtl_jvm_prog G (make_Cert G Phi)"
-proof (simp only: wt_jvm_prog_def)
+proof (unfold wt_jvm_prog_def)
 
   assume wfprog: 
     "wf_prog (\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G"
@@ -449,12 +439,12 @@
              (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> 
                (\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \<and>
              unique ms \<and>
-             (case sc of None \<Rightarrow> C = Object
-              | Some D \<Rightarrow>
+             (case sc of None => C = Object
+              | Some D =>
                   is_class G D \<and>
                   (D, C) \<notin> (subcls1 G)^* \<and>
                   (\<forall>(sig,rT,b)\<in>set ms. 
-                   \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \<longrightarrow> G\<turnstile>rT\<preceq>rT'))"
+                   \<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') --> G\<turnstile>rT\<preceq>rT'))"
              "(a, aa, ab, b) \<in> set G"
   
     assume uG : "unique G" 
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -11,31 +11,31 @@
 lemmas [simp del] = split_paired_Ex split_paired_All
 
 constdefs
-fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> bool"
-"fits phi is G rT s0 cert \<equiv> 
-  (\<forall>pc s1. pc < length is \<longrightarrow>
-    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \<longrightarrow>
-    (case cert!pc of None   \<Rightarrow> phi!pc = s1
-                   | Some t \<Rightarrow> phi!pc = Some t)))"
+fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
+"fits phi is G rT s0 cert == 
+  (\<forall>pc s1. pc < length is -->
+    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 -->
+    (case cert!pc of None   => phi!pc = s1
+                   | Some t => phi!pc = Some t)))"
 
 constdefs
-make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> method_type"
-"make_phi is G rT s0 cert \<equiv> 
+make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
+"make_phi is G rT s0 cert == 
    map (\<lambda>pc. case cert!pc of 
-               None   \<Rightarrow> val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
-             | Some t \<Rightarrow> Some t) [0..length is(]"
+               None   => val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
+             | Some t => Some t) [0..length is(]"
 
 
 lemma fitsD_None:
-  "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
+  "[|fits phi is G rT s0 cert; pc < length is;
     wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
-    cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
+    cert ! pc = None|] ==> phi!pc = s1"
   by (auto simp add: fits_def)
 
 lemma fitsD_Some:
-  "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
+  "[|fits phi is G rT s0 cert; pc < length is;
     wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
-    cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
+    cert ! pc = Some t|] ==> phi!pc = Some t"
   by (auto simp add: fits_def)
 
 lemma make_phi_Some:
@@ -62,7 +62,7 @@
   
 lemma fits_lemma1:
   "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
-  ==> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
+  ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
 proof (intro strip)
   fix pc t 
   assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
@@ -114,11 +114,11 @@
     "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
     by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
 
-  hence c1: "\<And>t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
+  hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
     by (simp add: wtl_cert_def split: if_splits)
   moreover
   from fits pc wts
-  have c2: "\<And>t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
+  have c2: "!!t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
     by - (drule fitsD_Some, auto)
   moreover
   from fits pc wts
@@ -150,7 +150,7 @@
 
   from fits wtl pc
   have cert_Some: 
-    "\<And>t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
+    "!!t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
     by (auto dest: fits_lemma1)
   
   from fits wtl pc
@@ -236,7 +236,7 @@
     by (rule fitsD_None)
   moreover    
   from fits pc wt0
-  have "\<And>t. cert!0 = Some t ==> phi!0 = cert!0"
+  have "!!t. cert!0 = Some t ==> phi!0 = cert!0"
     by - (drule fitsD_Some, auto)
   moreover
   from pc
@@ -247,7 +247,7 @@
     "wtl_cert x G rT s cert (length is) 0 = Ok s'"
     by simp (elim, rule that, simp)
   hence 
-    "\<And>t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
+    "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
     by (simp add: wtl_cert_def split: if_splits)
 
   ultimately
@@ -268,7 +268,7 @@
 
   with wtl
   have allpc:
-    "\<forall>pc. pc < length ins \<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
+    "\<forall>pc. pc < length ins --> wt_instr (ins ! pc) G rT phi (length ins) pc"
     by (blast intro: wtl_fits_wt)
 
   from pc wtl fits
@@ -279,15 +279,6 @@
   show ?thesis by (auto simp add: wt_method_def)
 qed
 
-lemma unique_set:
-  "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> (a',b',c',d') \<in> set l \<longrightarrow> 
-   a = a' \<longrightarrow> b=b' \<and> c=c' \<and> d=d'"
-  by (induct "l") auto
-
-lemma unique_epsilon:
-  "(a,b,c,d)\<in>set l \<longrightarrow> unique l \<longrightarrow> 
-   (\<epsilon> (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
-  by (auto simp add: unique_set)
 
 theorem wtl_correct:
 "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
@@ -304,9 +295,9 @@
     (is "\<exists>Phi. ?Q Phi")
   proof (intro exI)
     let "?Phi" = "\<lambda> C sig. 
-      let (C,x,y,mdecls) = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
-          (sig,rT,maxl,b) = \<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
-      in \<epsilon> phi. wt_method G C (snd sig) rT maxl b phi"
+      let (C,x,y,mdecls) = SOME (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+          (sig,rT,maxl,b) = SOME (sg,rT,maxl,b). (sg,rT,maxl,b) \<in> set mdecls \<and> sg = sig
+      in SOME phi. wt_method G C (snd sig) rT maxl b phi"
     from wtl_prog
     show "?Q ?Phi"
     proof (unfold wf_cdecl_def, intro)
@@ -328,8 +319,8 @@
               wt_method G a (snd sig) rT maxl b 
                ((\<lambda>(C,x,y,mdecls).
                     (\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
-                     (\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
-                 (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
+                     (SOME (sg,rT,maxl,b). (sg, rT, maxl, b) \<in> set mdecls \<and> sg = sig))
+                 (SOME (Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
           by - (drule bspec, assumption, 
                 clarsimp dest!: wtl_method_correct,
                 clarsimp intro!: someI simp add: unique_epsilon) 
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -11,44 +11,36 @@
 
 types
   certificate       = "state_type option list" 
-  class_certificate = "sig \<Rightarrow> certificate"
-  prog_certificate  = "cname \<Rightarrow> class_certificate"
+  class_certificate = "sig => certificate"
+  prog_certificate  = "cname => class_certificate"
 
 
 constdefs
   check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count]
-                 \<Rightarrow> bool"
-  "check_cert i G s cert pc max_pc \<equiv> \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>  
-                                     (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')"
+                 => bool"
+  "check_cert i G s cert pc max_pc == \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>  
+                                     (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')"
 
   wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] 
-               \<Rightarrow> state_type option err" 
-  "wtl_inst i G rT s cert max_pc pc \<equiv> 
+               => state_type option err" 
+  "wtl_inst i G rT s cert max_pc pc == 
      if app i G rT s \<and> check_cert i G s cert pc max_pc then 
        if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1))
      else Err";
 
-lemma wtl_inst_Ok:
-"(wtl_inst i G rT s cert max_pc pc = Ok s') =
- (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). 
-                   pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')) \<and> 
- (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
-  by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
-
-
 constdefs
   wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] 
-               \<Rightarrow> state_type option err"  
-  "wtl_cert i G rT s cert max_pc pc \<equiv>
+               => state_type option err"  
+  "wtl_cert i G rT s cert max_pc pc ==
      case cert!pc of
-        None    \<Rightarrow> wtl_inst i G rT s cert max_pc pc
-      | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then 
+        None    => wtl_inst i G rT s cert max_pc pc
+      | Some s' => if G \<turnstile> s <=' (Some s') then 
                     wtl_inst i G rT (Some s') cert max_pc pc 
                   else Err"
 
 consts 
   wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, 
-                     state_type option] \<Rightarrow> state_type option err"
+                     state_type option] => state_type option err"
 primrec
   "wtl_inst_list []     G rT cert max_pc pc s = Ok s"
   "wtl_inst_list (i#is) G rT cert max_pc pc s = 
@@ -57,19 +49,26 @@
               
 
 constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool"  
- "wtl_method G C pTs rT mxl ins cert \<equiv>  
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] => bool"  
+ "wtl_method G C pTs rT mxl ins cert ==  
 	let max_pc = length ins  
   in 
   0 < max_pc \<and>   
   wtl_inst_list ins G rT cert max_pc 0 
                 (Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err"
 
- wtl_jvm_prog :: "[jvm_prog,prog_certificate] \<Rightarrow> bool" 
- "wtl_jvm_prog G cert \<equiv>  
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" 
+ "wtl_jvm_prog G cert ==  
   wf_prog (\<lambda>G C (sig,rT,maxl,b). wtl_method G C (snd sig) rT maxl b (cert C sig)) G"
 
-text {* \medskip *} 
+
+
+lemma wtl_inst_Ok:
+"(wtl_inst i G rT s cert max_pc pc = Ok s') =
+ (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). 
+                   pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and> 
+ (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
+  by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
 
 lemma strict_Some [simp]: 
 "(strict f x = Ok y) = (\<exists> z. x = Ok z \<and> f z = Ok y)"
@@ -127,7 +126,7 @@
 qed
 
 lemma take_Suc:
-  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+  "\<forall>n. n < length l --> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
 proof (induct l)
   show "?P []" by simp
 
@@ -191,4 +190,14 @@
     by (auto simp add: wtl_append min_def)
 qed
 
+lemma unique_set:
+"(a,b,c,d)\<in>set l --> unique l --> (a',b',c',d') \<in> set l --> 
+  a = a' --> b=b' \<and> c=c' \<and> d=d'"
+  by (induct "l") auto
+
+lemma unique_epsilon:
+  "(a,b,c,d)\<in>set l --> unique l --> 
+  (SOME (a',b',c',d'). (a',b',c',d') \<in> set l \<and> a'=a) = (a,b,c,d)"
+  by (auto simp add: unique_set)
+
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/Step.thy
--- a/src/HOL/MicroJava/BV/Step.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -12,7 +12,7 @@
 
 text "Effect of instruction on the state type:"
 consts 
-step' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
+step' :: "instr \<times> jvm_prog \<times> state_type => state_type"
 
 recdef step' "{}"
 "step' (Load idx,  G, (ST, LT))          = (val (LT ! idx) # ST, LT)"
@@ -40,13 +40,13 @@
 (* "step' (i,G,s)                           = None" *)
 
 constdefs
-  step :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
-  "step i G \<equiv> opt_map (\<lambda>s. step' (i,G,s))"
+  step :: "instr => jvm_prog => state_type option => state_type option"
+  "step i G == option_map (\<lambda>s. step' (i,G,s))"
 
 
 text "Conditions under which step is applicable:"
 consts
-app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
+app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type => bool"
 
 recdef app' "{}"
 "app' (Load idx, G, rT, s)                  = (idx < length (snd s) \<and> 
@@ -88,13 +88,13 @@
 
 
 constdefs
-  app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> ty \<Rightarrow> state_type option \<Rightarrow> bool"
-  "app i G rT s \<equiv> case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,rT,t)"
+  app :: "instr => jvm_prog => ty => state_type option => bool"
+  "app i G rT s == case s of None => True | Some t => app' (i,G,rT,t)"
 
 text {* program counter of successor instructions: *}
 
 consts
-succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"
+succs :: "instr => p_count => p_count list"
 
 primrec 
 "succs (Load idx) pc         = [pc+1]"
@@ -117,13 +117,13 @@
 "succs (Invoke C mn fpTs) pc = [pc+1]"
 
 
-lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
+lemma 1: "2 < length a ==> (\<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) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
+lemma 2: "\<not>(2 < length a) ==> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
 proof -;
   assume "\<not>(2 < length a)"
   hence "length a < (Suc 2)" by simp
@@ -136,7 +136,7 @@
     hence "\<exists> l. x = [l]"  by - (cases x, auto)
   } note 0 = this
 
-  have "length a = 2 \<Longrightarrow> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+  have "length a = 2 ==> \<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
   with * show ?thesis by (auto dest: 0)
 qed
 
@@ -149,7 +149,6 @@
   by (simp add: app_def)
 
 
-
 lemma appLoad[simp]:
 "(app (Load idx) G rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err)"
   by (simp add: app_def)
@@ -264,7 +263,7 @@
   method (G,C) (mn,fpTs) = Some (mD', rT', b'))" (is "?app s = ?P s")
 proof (cases (open) s)
   case Pair
-  have "?app (a,b) \<Longrightarrow> ?P (a,b)"
+  have "?app (a,b) ==> ?P (a,b)"
   proof -
     assume app: "?app (a,b)"
     hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> 
@@ -286,7 +285,7 @@
     with app
     show ?thesis by (auto simp add: app_def) blast
   qed
-  with Pair have "?app s \<Longrightarrow> ?P s" by simp
+  with Pair have "?app s ==> ?P s" by simp
   thus ?thesis by (auto simp add: app_def)
 qed 
 
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -14,7 +14,7 @@
 
 
 lemma sup_loc_some [rule_format]:
-"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow> 
+"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = Ok t --> 
   (\<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 \<longrightarrow> 
+"\<forall>b. length a = length b --> 
      (\<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 \<longrightarrow> ?Q a b" is "?P a")
+ (is "\<forall>b. length a = length b --> ?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 \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
+"\<forall>n. n \<le> length x --> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
 proof (induct (open) ?P x)
   show "?P []" by simp
 
@@ -94,7 +94,7 @@
 
 
 lemma rev_append_cons:
-"\<lbrakk>n < length x\<rbrakk> \<Longrightarrow> \<exists>a b c. x = (rev a) @ b # c \<and> length a = n"
+"[|n < length x|] ==> \<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
@@ -118,7 +118,7 @@
 
 
 lemma app_mono: 
-"\<lbrakk>G \<turnstile> s <=' s'; app i G rT s'\<rbrakk> \<Longrightarrow> app i G rT s";
+"[|G \<turnstile> s <=' s'; app i G rT s'|] ==> app i G rT s";
 proof -
 
   { fix s1 s2
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Conform.ML
--- a/src/HOL/MicroJava/J/Conform.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -6,25 +6,25 @@
 
 section "hext";
 
-val hextI = prove_goalw thy [hext_def] "\\<And>h. \
-\ \\<forall>a C fs . h  a = Some (C,fs) \\<longrightarrow>  \
-\     (\\<exists>fs'. h' a = Some (C,fs')) \\<Longrightarrow> h\\<le>|h'" (K [Auto_tac ]);
+val hextI = prove_goalw thy [hext_def] "!!h. \
+\ \\<forall>a C fs . h  a = Some (C,fs) -->  \
+\     (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'" (K [Auto_tac ]);
 
 val hext_objD = prove_goalw thy [hext_def] 
-"\\<And>h. \\<lbrakk>h\\<le>|h'; h a = Some (C,fs) \\<rbrakk> \\<Longrightarrow> \\<exists>fs'. h' a = Some (C,fs')" 
+"!!h. [|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')" 
 	(K [Force_tac 1]);
 
 val hext_refl = prove_goal thy "h\\<le>|h" (K [
 	rtac hextI 1,
 	Fast_tac 1]);
 
-val hext_new = prove_goal thy "\\<And>h. h a = None \\<Longrightarrow> h\\<le>|h(a\\<mapsto>x)" (K [
+val hext_new = prove_goal thy "!!h. h a = None ==> h\\<le>|h(a\\<mapsto>x)" (K [
 	rtac hextI 1,
 	safe_tac HOL_cs,
 	 ALLGOALS (case_tac "aa = a"),
 	   Auto_tac]);
 
-val hext_trans = prove_goal thy "\\<And>h. \\<lbrakk>h\\<le>|h'; h'\\<le>|h''\\<rbrakk> \\<Longrightarrow> h\\<le>|h''" (K [
+val hext_trans = prove_goal thy "!!h. [|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''" (K [
 	rtac hextI 1,
 	safe_tac HOL_cs,
 	 fast_tac (HOL_cs addDs [hext_objD]) 1]);
@@ -32,7 +32,7 @@
 Addsimps [hext_refl, hext_new];
 
 val hext_upd_obj = prove_goal thy 
-"\\<And>h. h a = Some (C,fs) \\<Longrightarrow> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
+"!!h. h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
 	rtac hextI 1,
 	safe_tac HOL_cs,
 	 ALLGOALS (case_tac "aa = a"),
@@ -42,37 +42,37 @@
 section "conf";
 
 val conf_Null = prove_goalw thy [conf_def] 
-"G,h\\<turnstile>Null\\<Colon>\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
+"G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
 Addsimps [conf_Null];
 
 val conf_litval = prove_goalw thy [conf_def] 
-"typeof (\\<lambda>v. None) v = Some T \\<longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T" (K [
+"typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T" (K [
 	rtac val_.induct 1,
 	    Auto_tac]) RS mp;
 
-Goalw [conf_def] "G,s\\<turnstile>Unit\\<Colon>\\<preceq>PrimT Void";
+Goalw [conf_def] "G,s\\<turnstile>Unit::\\<preceq>PrimT Void";
 by( Simp_tac 1);
 qed "conf_VoidI";
 
-Goalw [conf_def] "G,s\\<turnstile>Bool b\\<Colon>\\<preceq>PrimT Boolean";
+Goalw [conf_def] "G,s\\<turnstile>Bool b::\\<preceq>PrimT Boolean";
 by( Simp_tac 1);
 qed "conf_BooleanI";
 
-Goalw [conf_def] "G,s\\<turnstile>Intg i\\<Colon>\\<preceq>PrimT Integer";
+Goalw [conf_def] "G,s\\<turnstile>Intg i::\\<preceq>PrimT Integer";
 by( Simp_tac 1);
 qed "conf_IntegerI";
 
 Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
 
 val conf_AddrI = prove_goalw thy [conf_def] 
-"\\<And>G. \\<lbrakk>h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>T"
+"!!G. [|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T"
 (K [Asm_full_simp_tac 1]);
 
 val conf_obj_AddrI = prove_goalw thy [conf_def]
- "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq> Class D" 
+ "!!G. [|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D" 
 (K [Asm_full_simp_tac 1]);
 
-Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
+Goalw [conf_def] "is_type G T --> G,h\\<turnstile>default_val T::\\<preceq>T";
 by (res_inst_tac [("y","T")] ty.exhaust 1);
 by  (etac ssubst 1);
 by  (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
@@ -80,7 +80,7 @@
 qed_spec_mp "defval_conf";
 
 val conf_upd_obj = prove_goalw thy [conf_def] 
-"h a = Some (C,fs) \\<longrightarrow> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x\\<Colon>\\<preceq>T) = (G,h\\<turnstile>x\\<Colon>\\<preceq>T)" (fn _ => [
+"h a = Some (C,fs) --> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)" (fn _ => [
 	rtac impI 1,
 	rtac val_.induct 1,
 	 ALLGOALS Simp_tac,
@@ -88,14 +88,14 @@
 	 ALLGOALS Asm_simp_tac]) RS mp;
 
 val conf_widen = prove_goalw thy [conf_def] 
-"\\<And>G. wf_prog wf_mb G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
+"!!G. wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'" (K [
 	rtac val_.induct 1,
 	    ALLGOALS Simp_tac,
 	    ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
 bind_thm ("conf_widen", conf_widen);
 
 val conf_hext' = prove_goalw thy [conf_def] 
-	"\\<And>h. h\\<le>|h' \\<Longrightarrow> (\\<forall>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)" (K [
+	"!!h. h\\<le>|h' ==> (\\<forall>v T. G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T)" (K [
 	REPEAT (rtac allI 1),
 	rtac val_.induct 1,
 	 ALLGOALS Simp_tac,
@@ -107,36 +107,36 @@
 bind_thm ("conf_hext", conf_hext);
 
 val new_locD = prove_goalw thy [conf_def] 
-	"\\<lbrakk>h a = None; G,h\\<turnstile>Addr t\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> t\\<noteq>a" (fn prems => [
+	"[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a" (fn prems => [
 	cut_facts_tac prems 1,
 	Full_simp_tac 1,
 	safe_tac HOL_cs,
 	Asm_full_simp_tac 1]);
 
 Goalw [conf_def]
- "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> a' = Null |  \
+ "G,h\\<turnstile>a'::\\<preceq>RefT T --> a' = Null |  \
 \ (\\<exists>a obj T'. a' = Addr a \\<and>  h a = Some obj \\<and>  obj_ty obj = T' \\<and>  G\\<turnstile>T'\\<preceq>RefT T)";
 by(induct_tac "a'" 1);
 by(Auto_tac);
 qed_spec_mp "conf_RefTD";
 
-val conf_NullTD = prove_goal thy "\\<And>G. G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT NullT \\<Longrightarrow> a' = Null" (K [
+val conf_NullTD = prove_goal thy "!!G. G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null" (K [
 	dtac conf_RefTD 1,
 	Step_tac 1,
 	 Auto_tac]);
 
-val non_npD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t\\<rbrakk> \\<Longrightarrow> \
+val non_npD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
 \ \\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t" (K [
 	dtac conf_RefTD 1,
 	Step_tac 1,
 	 Auto_tac]);
 
-val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
+val non_np_objD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
 \ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>C'\\<preceq>C C)" 
 	(K[fast_tac (claset() addDs [non_npD]) 1]);
 
-Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wf_mb G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
-\ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
+Goal "a' \\<noteq> Null --> wf_prog wf_mb G --> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
+\ (\\<forall>C. t = ClassT C --> C \\<noteq> Object) --> \
 \ (\\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t)";
 by(rtac impI 1);
 by(rtac impI 1);
@@ -150,7 +150,7 @@
 by(Fast_tac 1);
 qed_spec_mp "non_np_objD'";
 
-Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow>  list_all2 (conf G h) vs Ts'";
+Goal "wf_prog wf_mb G ==> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'";
 by(induct_tac "vs" 1);
  by(ALLGOALS Clarsimp_tac);
 by(forward_tac [list_all2_lengthD RS sym] 1);
@@ -166,30 +166,30 @@
 section "lconf";
 
 val lconfD = prove_goalw thy [lconf_def] 
-   "\\<And>X. \\<lbrakk> G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts; Ts n = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>(the (vs n))\\<Colon>\\<preceq>T"
+   "!!X. [| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T"
  (K [Force_tac 1]);
 
 val lconf_hext = prove_goalw thy [lconf_def] 
-	"\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]L; h\\<le>|h' \\<rbrakk> \\<Longrightarrow> G,h'\\<turnstile>l[\\<Colon>\\<preceq>]L" (K [
+	"!!X. [| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L" (K [
 		fast_tac (claset() addEs [conf_hext]) 1]);
 AddEs [lconf_hext];
 
-Goalw [lconf_def] "\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT; \
-\ G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>l(va\\<mapsto>v)[\\<Colon>\\<preceq>]lT";
+Goalw [lconf_def] "!!X. [| G,h\\<turnstile>l[::\\<preceq>]lT; \
+\ G,h\\<turnstile>v::\\<preceq>T; lT va = Some T |] ==> G,h\\<turnstile>l(va\\<mapsto>v)[::\\<preceq>]lT";
 by( Clarify_tac 1);
 by( case_tac "n = va" 1);
  by Auto_tac;
 qed "lconf_upd";
 
-Goal "\\<forall>x. P x \\<longrightarrow> R (dv x) x \\<Longrightarrow> (\\<forall>x. map_of fs f = Some x \\<longrightarrow> P x) \\<longrightarrow> \
-\ (\\<forall>T. map_of fs f = Some T \\<longrightarrow> \
+Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
+\ (\\<forall>T. map_of fs f = Some T --> \
 \ (\\<exists>v. map_of (map (\\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \\<and>  R v T))";
 by( induct_tac "fs" 1);
 by Auto_tac;
 qed_spec_mp "lconf_init_vars_lemma";
 
 Goalw [lconf_def, init_vars_def] 
-"\\<forall>n. \\<forall>T. map_of fs n = Some T \\<longrightarrow> is_type G T \\<Longrightarrow> G,h\\<turnstile>init_vars fs[\\<Colon>\\<preceq>]map_of fs";
+"\\<forall>n. \\<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\\<turnstile>init_vars fs[::\\<preceq>]map_of fs";
 by Auto_tac;
 by( rtac lconf_init_vars_lemma 1);
 by(   atac 3);
@@ -200,10 +200,10 @@
 AddSIs [lconf_init_vars];
 
 val lconf_ext = prove_goalw thy [lconf_def] 
-"\\<And>X. \\<lbrakk>G,s\\<turnstile>l[\\<Colon>\\<preceq>]L; G,s\\<turnstile>v\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,s\\<turnstile>l(vn\\<mapsto>v)[\\<Colon>\\<preceq>]L(vn\\<mapsto>T)" 
+"!!X. [|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)" 
 	(K [Auto_tac]);
 
-Goalw [lconf_def] "G,h\\<turnstile>l[\\<Colon>\\<preceq>]L \\<Longrightarrow> \\<forall>vs Ts. nodups vns \\<longrightarrow> length Ts = length vns \\<longrightarrow> list_all2 (\\<lambda>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts \\<longrightarrow> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[\\<Colon>\\<preceq>]L(vns[\\<mapsto>]Ts)";
+Goalw [lconf_def] "G,h\\<turnstile>l[::\\<preceq>]L ==> \\<forall>vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\\<lambda>v T. G,h\\<turnstile>v::\\<preceq>T) vs Ts --> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[::\\<preceq>]L(vns[\\<mapsto>]Ts)";
 by( induct_tac "vns" 1);
 by(  ALLGOALS Clarsimp_tac);
 by( forward_tac [list_all2_lengthD] 1);
@@ -214,10 +214,10 @@
 section "oconf";
 
 val oconf_hext = prove_goalw thy [oconf_def] 
-"\\<And>X. G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> h\\<le>|h' \\<Longrightarrow> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
+"!!X. G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
 
 val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
-\ (\\<forall>T f. map_of(fields (G,C)) f = Some T \\<longrightarrow> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v\\<Colon>\\<preceq>T))"(K [
+\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v::\\<preceq>T))"(K [
 	Auto_tac]);
 
 val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
@@ -225,11 +225,11 @@
 
 section "hconf";
 
-Goalw [hconf_def] "\\<lbrakk>G\\<turnstile>h h\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
+Goalw [hconf_def] "[|G\\<turnstile>h h\\<surd>; h a = Some obj|] ==> G,h\\<turnstile>obj\\<surd>";
 by (Fast_tac 1);
 qed "hconfD";
 
-Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G\\<turnstile>h h\\<surd>";
+Goalw [hconf_def] "\\<forall>a obj. h a=Some obj --> G,h\\<turnstile>obj\\<surd> ==> G\\<turnstile>h h\\<surd>";
 by (Fast_tac 1);
 qed "hconfI";
 
@@ -237,25 +237,25 @@
 section "conforms";
 
 val conforms_heapD = prove_goalw thy [conforms_def]
-	"(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G\\<turnstile>h h\\<surd>"
+	"(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>"
 	(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
 
 val conforms_localD = prove_goalw thy [conforms_def]
-	 "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT" (fn prems => [
+	 "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT" (fn prems => [
 	cut_facts_tac prems 1, Asm_full_simp_tac 1]);
 
 val conformsI = prove_goalw thy [conforms_def] 
-"\\<lbrakk>G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
+"[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)" (fn prems => [
 	cut_facts_tac prems 1,
 	Simp_tac 1,
 	Auto_tac]);
 
-Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
+Goal "[|(h,l)::\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> |] ==> (h',l)::\\<preceq>(G,lT)";
 by( fast_tac (HOL_cs addDs [conforms_localD] 
   addSEs [conformsI, lconf_hext]) 1);
 qed "conforms_hext";
 
-Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)\\<rbrakk> \\<Longrightarrow> (h(a\\<mapsto>obj),l)\\<Colon>\\<preceq>(G, lT)";
+Goal "[|(h,l)::\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)|] ==> (h(a\\<mapsto>obj),l)::\\<preceq>(G, lT)";
 by( rtac conforms_hext 1);
 by   Auto_tac;
 by( rtac hconfI 1);
@@ -265,7 +265,7 @@
 qed "conforms_upd_obj";
 
 Goalw [conforms_def] 
-"\\<lbrakk>(h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T\\<rbrakk> \\<Longrightarrow> \
-\ (h, l(va\\<mapsto>v))\\<Colon>\\<preceq>(G, lT)";
+"[|(h, l)::\\<preceq>(G, lT); G,h\\<turnstile>v::\\<preceq>T; lT va = Some T|] ==> \
+\ (h, l(va\\<mapsto>v))::\\<preceq>(G, lT)";
 by( auto_tac (claset() addEs [lconf_upd], simpset()));
 qed "conforms_upd_local";
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -12,23 +12,23 @@
 
 constdefs
 
-  hext :: "aheap \\<Rightarrow> aheap \\<Rightarrow> bool"		 (     "_\\<le>|_"  [51,51] 50)
- "h\\<le>|h' \\<equiv> \\<forall>a C fs. h a = Some(C,fs) \\<longrightarrow> (\\<exists>fs'. h' a = Some(C,fs'))"
+  hext :: "aheap => aheap => bool"		 (     "_\\<le>|_"  [51,51] 50)
+ "h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))"
 
-  conf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> ty \\<Rightarrow> bool"	 ( "_,_\\<turnstile>_\\<Colon>\\<preceq>_"  [51,51,51,51] 50)
- "G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<equiv> \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
+  conf :: "'c prog => aheap => val => ty => bool"	 ( "_,_\\<turnstile>_::\\<preceq>_"  [51,51,51,51] 50)
+ "G,h\\<turnstile>v::\\<preceq>T == \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
 
-  lconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> ('a \\<leadsto> val) \\<Rightarrow> ('a \\<leadsto> ty) \\<Rightarrow> bool"
-                                                 ("_,_\\<turnstile>_[\\<Colon>\\<preceq>]_" [51,51,51,51] 50)
- "G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts \\<equiv> \\<forall>n T. Ts n = Some T \\<longrightarrow> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T)"
+  lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
+                                                 ("_,_\\<turnstile>_[::\\<preceq>]_" [51,51,51,51] 50)
+ "G,h\\<turnstile>vs[::\\<preceq>]Ts == \\<forall>n T. Ts n = Some T --> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T)"
 
-  oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
- "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))"
+  oconf :: "'c prog => aheap => obj => bool"      ("_,_\\<turnstile>_\\<surd>"     [51,51,51]    50)
+ "G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))"
 
-  hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
- "G\\<turnstile>h h\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
+  hconf :: "'c prog => aheap => bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
+ "G\\<turnstile>h h\\<surd>    == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>"
 
-  conforms :: "state \\<Rightarrow> java_mb env_ \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
- "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
+  conforms :: "state => java_mb env_ => bool"	 ("_::\\<preceq>_"       [51,51]       50)
+ "s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Decl.ML
--- a/src/HOL/MicroJava/J/Decl.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Decl.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -8,8 +8,8 @@
 	rtac finite_map_of 1]);
 
 val is_classI = prove_goalw thy [is_class_def]
-"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
+"!!G. class G C = Some c ==> is_class G C" (K [Auto_tac]);
 
 val is_classD = prove_goalw thy [is_class_def]
-"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
+"!!G. is_class G C ==> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
 	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -32,26 +32,26 @@
 
 defs 
 
- ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
+ ObjectC_def "ObjectC == (Object, (None, [], []))"
 
 
 types 'c prog = "'c cdecl list"
 
 consts
 
-  class		:: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
+  class		:: "'c prog => (cname \\<leadsto> 'c class)"
 
-  is_class	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
-  is_type	:: "'c prog \\<Rightarrow> ty    \\<Rightarrow> bool"
+  is_class	:: "'c prog => cname => bool"
+  is_type	:: "'c prog => ty    => bool"
 
 defs
 
-  class_def	"class        \\<equiv> map_of"
+  class_def	"class        == map_of"
 
-  is_class_def	"is_class G C \\<equiv> class G C \\<noteq> None"
+  is_class_def	"is_class G C == class G C \\<noteq> None"
 
 primrec
 "is_type G (PrimT pt) = True"
-"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
+"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Eval.ML
--- a/src/HOL/MicroJava/J/Eval.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -4,44 +4,44 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-Goal "\\<lbrakk>new_Addr (heap s) = (a,x); \
-\      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)\\<rbrakk> \\<Longrightarrow> \
-\      G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> s'";
+Goal "[|new_Addr (heap s) = (a,x); \
+\      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
+\      G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
 by (hyp_subst_tac 1);
 br eval_evals_exec.NewC 1;
 by Auto_tac;
 qed "NewCI";
 
-Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ>  v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
-\             (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
-\             (G\\<turnstile>(x,s) -c       \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)";
+Goal "!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x'=None --> x=None) \\<and> \
+\             (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x'=None --> x=None) \\<and> \
+\             (G\\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)";
 by(split_all_tac 1);
 by(rtac eval_evals_exec.induct 1);
 by(rewtac c_hupd_def);
 by(ALLGOALS Asm_full_simp_tac);
 qed "eval_evals_exec_no_xcpt";
 
-val eval_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e\\<succ>v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
+val eval_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None" (K [
 	dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
 	Fast_tac 1]);
-val evals_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e[\\<succ>]v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
+val evals_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None" (K [
 	dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
 	Fast_tac 1]);
 
 val eval_evals_exec_xcpt = prove_goal thy 
-"\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ>  v \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
-\        (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
-\        (G\\<turnstile>(x,s) -c       \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s)"
+"!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
+\        (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
+\        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)"
  (K [
 	split_all_tac 1,
 	rtac eval_evals_exec.induct 1,
 	rewtac c_hupd_def,
 	ALLGOALS Asm_full_simp_tac]);
 val eval_xcpt = prove_goal thy 
-"\\<And>X. G\\<turnstile>(Some xc,s) -e\\<succ>v\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and>  s'=s" (K [
+"!!X. G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
 	dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
 	Fast_tac 1]);
 val exec_xcpt = prove_goal thy 
-"\\<And>X. G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and>  s'=s" (K [
+"!!X. G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
 	dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
 	Fast_tac 1]);
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -10,118 +10,118 @@
 Eval = State + WellType +
 
 consts
-  eval  :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr      \\<times> val      \\<times> xstate) set"
-  evals :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
-  exec  :: "java_mb prog \\<Rightarrow> (xstate \\<times> stmt                 \\<times> xstate) set"
+  eval  :: "java_mb prog => (xstate \\<times> expr      \\<times> val      \\<times> xstate) set"
+  evals :: "java_mb prog => (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
+  exec  :: "java_mb prog => (xstate \\<times> stmt                 \\<times> xstate) set"
 
 syntax
-  eval :: "[java_mb prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
+  eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "("_\\<turnstile>_ -_\\<succ>_-> _"[51,82,82,82,82]81)
   evals:: "[java_mb prog,xstate,expr list,
-	                      val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81)
-  exec :: "[java_mb prog,xstate,stmt,    xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _"  [51,82,82,   82]81)
+	                      val list,xstate] => bool "("_\\<turnstile>_ -_[\\<succ>]_-> _"[51,82,51,51,82]81)
+  exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "("_\\<turnstile>_ -_-> _"  [51,82,82,   82]81)
 
 translations
-  "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" <= "(s, e, v, x, s') \\<in> eval  G"
-  "G\\<turnstile>s -e \\<succ> v\\<rightarrow>    s' " == "(s, e, v,    s' ) \\<in> eval  G"
-  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
-  "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow>    s' " == "(s, e, v,    s' ) \\<in> evals G"
-  "G\\<turnstile>s -c    \\<rightarrow> (x,s')" <= "(s, c, x, s') \\<in> exec  G"
-  "G\\<turnstile>s -c    \\<rightarrow>    s' " == "(s, c,    s') \\<in> exec  G"
+  "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval  G"
+  "G\\<turnstile>s -e \\<succ> v->    s' " == "(s, e, v,    s' ) \\<in> eval  G"
+  "G\\<turnstile>s -e[\\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
+  "G\\<turnstile>s -e[\\<succ>]v->    s' " == "(s, e, v,    s' ) \\<in> evals G"
+  "G\\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \\<in> exec  G"
+  "G\\<turnstile>s -c    ->    s' " == "(s, c,    s') \\<in> exec  G"
 
 inductive "eval G" "evals G" "exec G" intrs
 
 (* evaluation of expressions *)
 
   (* cf. 15.5 *)
-  XcptE				  "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary\\<rightarrow> (Some xc,s)"
+  XcptE				  "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
 
   (* cf. 15.8.1 *)
-  NewC	"\\<lbrakk>h = heap s; (a,x) = new_Addr h;
-	  h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))\\<rbrakk> \\<Longrightarrow>
-				   G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> c_hupd h' (x,s)"
+  NewC	"[|h = heap s; (a,x) = new_Addr h;
+	  h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))|] ==>
+				   G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
 
   (* cf. 15.15 *)
-  Cast	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> (x1,s1);
-	  x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
-			        G\\<turnstile>Norm s0 -Cast C e\\<succ>v\\<rightarrow> (x2,s1)"
+  Cast	"[|G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
+	  x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1|] ==>
+			        G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
 
   (* cf. 15.7.1 *)
-  Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
+  Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
 
-  BinOp "\\<lbrakk>G\\<turnstile>Norm s -e1\\<succ>v1\\<rightarrow> s1;
-	  G\\<turnstile>s1     -e2\\<succ>v2\\<rightarrow> s2;
-	  v = (case bop of Eq  \\<Rightarrow> Bool (v1 = v2)
-	                 | Add \\<Rightarrow> Intg (the_Intg v1 + the_Intg v2))\\<rbrakk> \\<Longrightarrow>
-				   G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v\\<rightarrow> s2"
+  BinOp "[|G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
+	  G\\<turnstile>s1     -e2\\<succ>v2-> s2;
+	  v = (case bop of Eq  => Bool (v1 = v2)
+	                 | Add => Intg (the_Intg v1 + the_Intg v2))|] ==>
+				   G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
 
   (* cf. 15.13.1, 15.2 *)
-  LAcc				  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> Norm s"
+  LAcc				  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
 
   (* cf. 15.25.1 *)
-  LAss  "\\<lbrakk>G\\<turnstile>Norm s -e\\<succ>v\\<rightarrow>  (x,(h,l));
-	  l' = (if x = None then l(va\\<mapsto>v) else l)\\<rbrakk> \\<Longrightarrow>
-				   G\\<turnstile>Norm s -va\\<Colon>=e\\<succ>v\\<rightarrow> (x,(h,l'))"
+  LAss  "[|G\\<turnstile>Norm s -e\\<succ>v->  (x,(h,l));
+	  l' = (if x = None then l(va\\<mapsto>v) else l)|] ==>
+				   G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
 
 
   (* cf. 15.10.1, 15.2 *)
-  FAcc	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> (x1,s1); 
-	  v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))\\<rbrakk> \\<Longrightarrow>
-				 G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v\\<rightarrow> (np a' x1,s1)"
+  FAcc	"[|G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1); 
+	  v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))|] ==>
+				 G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
 
   (* cf. 15.25.1 *)
-  FAss  "\\<lbrakk>G\\<turnstile>     Norm s0  -e1\\<succ>a'\\<rightarrow> (x1,s1); a = the_Addr a';
-	  G\\<turnstile>(np a' x1,s1) -e2\\<succ>v \\<rightarrow> (x2,s2);
+  FAss  "[|G\\<turnstile>     Norm s0  -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
+	  G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
 	  h = heap s2; (c,fs) = the (h a);
-	  h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))\\<rbrakk> \\<Longrightarrow>
-			  G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)"
+	  h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))|] ==>
+			  G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
 
   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
-  Call	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
-	   G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a));
+  Call	"[|G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
+	   G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
 	   (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
-	   G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk\\<rightarrow> s3;
-	   G\\<turnstile>     s3 -res\\<succ>v \\<rightarrow> (x4,s4)\\<rbrakk> \\<Longrightarrow>
-			    G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v\\<rightarrow> (x4,(heap s4,l))"
+	   G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
+	   G\\<turnstile>     s3 -res\\<succ>v -> (x4,s4)|] ==>
+			    G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
 
 
 (* evaluation of expression lists *)
 
   (* cf. 15.5 *)
-  XcptEs			  "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary\\<rightarrow> (Some xc,s)"
+  XcptEs			  "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
 
   (* cf. 15.11.??? *)
   Nil
-				    "G\\<turnstile>Norm s0 -[][\\<succ>][]\\<rightarrow> Norm s0"
+				    "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
 
   (* cf. 15.6.4 *)
-  Cons	"\\<lbrakk>G\\<turnstile>Norm s0 -e  \\<succ> v \\<rightarrow> s1;
-           G\\<turnstile>     s1 -es[\\<succ>]vs\\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
-				   G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs\\<rightarrow> s2"
+  Cons	"[|G\\<turnstile>Norm s0 -e  \\<succ> v -> s1;
+           G\\<turnstile>     s1 -es[\\<succ>]vs-> s2|] ==>
+				   G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
 
 (* execution of statements *)
 
   (* cf. 14.1 *)
-  XcptS				 "G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (Some xc,s)"
+  XcptS				 "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)"
 
   (* cf. 14.5 *)
-  Skip	 			    "G\\<turnstile>Norm s -Skip\\<rightarrow> Norm s"
+  Skip	 			    "G\\<turnstile>Norm s -Skip-> Norm s"
 
   (* cf. 14.7 *)
-  Expr	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> s1\\<rbrakk> \\<Longrightarrow>
-				  G\\<turnstile>Norm s0 -Expr e\\<rightarrow> s1"
+  Expr	"[|G\\<turnstile>Norm s0 -e\\<succ>v-> s1|] ==>
+				  G\\<turnstile>Norm s0 -Expr e-> s1"
 
   (* cf. 14.2 *)
-  Comp	"\\<lbrakk>G\\<turnstile>Norm s0 -s \\<rightarrow> s1;
-	  G\\<turnstile>     s1 -t \\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
-				 G\\<turnstile>Norm s0 -(s;; t)\\<rightarrow> s2"
+  Comp	"[|G\\<turnstile>Norm s0 -s -> s1;
+	  G\\<turnstile>     s1 -t -> s2|] ==>
+				 G\\<turnstile>Norm s0 -(s;; t)-> s2"
 
   (* cf. 14.8.2 *)
-  Cond	"\\<lbrakk>G\\<turnstile>Norm s0  -e \\<succ>v\\<rightarrow> s1;
-	  G\\<turnstile>     s1 -(if  the_Bool v then s else t)\\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
-		        G\\<turnstile>Norm s0 -(If(e) s Else t)\\<rightarrow> s2"
+  Cond	"[|G\\<turnstile>Norm s0  -e \\<succ>v-> s1;
+	  G\\<turnstile>     s1 -(if  the_Bool v then s else t)-> s2|] ==>
+		        G\\<turnstile>Norm s0 -(If(e) s Else t)-> s2"
 
   (* cf. 14.10, 14.10.1 *)
-  Loop	"\\<lbrakk>G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)\\<rightarrow> s1\\<rbrakk> \\<Longrightarrow>
-			    G\\<turnstile>Norm s0 -(While(e) s)\\<rightarrow> s1"
+  Loop	"[|G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)-> s1|] ==>
+			    G\\<turnstile>Norm s0 -(While(e) s)-> s1"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -11,7 +11,7 @@
 val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"] 
 "map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
 val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"] 
-"\\<And>X. x\\<noteq>k \\<Longrightarrow> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
+"!!X. x\\<noteq>k ==> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
 Delsimps[map_of_Cons]; (* sic! *)
 Addsimps[map_of_Cons1, map_of_Cons2];
 
@@ -30,12 +30,12 @@
 	Simp_tac 1]);
 Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
 
-Goal "\\<And>X. (Object,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+Goal "!!X. (Object,C) \\<in> (subcls1 tprg)^+ ==> R";
 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
 qed "not_Object_subcls";
 AddSEs [not_Object_subcls];
 
-Goal "tprg\\<turnstile>Object\\<preceq>C C \\<Longrightarrow> C = Object";
+Goal "tprg\\<turnstile>Object\\<preceq>C C ==> C = Object";
 be rtrancl_induct 1;
 by  Auto_tac;
 bd subcls1D 1;
@@ -43,16 +43,16 @@
 qed "subcls_ObjectD";
 AddSDs[subcls_ObjectD];
 
-Goal "\\<And>X. (Base, Ext) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+Goal "!!X. (Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
 qed "not_Base_subcls_Ext";
 AddSEs [not_Base_subcls_Ext];
 
-Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z \\<Longrightarrow> C=Object \\<or> C=Base \\<or> C=Ext";
+Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
 by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
 qed "class_tprgD";
 
-Goal "(C,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
 by (ftac class_tprgD 1);
 by (auto_tac (claset() addSDs [],simpset()));
@@ -196,7 +196,7 @@
 
 fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
 Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ 
-\ Expr(e\\<Colon>=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
+\ Expr(e::=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
 (* ?pTs' = [Class Base] *)
 by t;		(* ;; *)
 by  t;		(* Expr *)
@@ -225,8 +225,8 @@
 Delsplits[split_if];
 Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
 Goalw [test_def] 
-" \\<lbrakk>new_Addr (heap (snd s0)) = (a, None)\\<rbrakk> \\<Longrightarrow> \
-\ tprg\\<turnstile>s0 -test\\<rightarrow> ?s";
+" [|new_Addr (heap (snd s0)) = (a, None)|] ==> \
+\ tprg\\<turnstile>s0 -test-> ?s";
 (* ?s = s3 *)
 by e;		(* ;; *)
 by  e;		(* Expr *)
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -35,8 +35,8 @@
 
 consts
 
-  cnam_ :: "cnam_ \\<Rightarrow> cname"
-  vnam_ :: "vnam_ \\<Rightarrow> vnam"
+  cnam_ :: "cnam_ => cname"
+  vnam_ :: "vnam_ => vnam"
 
 rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
 
@@ -74,18 +74,18 @@
 
 defs
 
-  foo_Base_def "foo_Base \\<equiv> ([x],[],Skip,LAcc x)"
-  BaseC_def "BaseC \\<equiv> (Base, (Some Object, 
+  foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
+  BaseC_def "BaseC == (Base, (Some Object, 
 			     [(vee, PrimT Boolean)], 
 			     [((foo,[Class Base]),Class Base,foo_Base)]))"
-  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast Ext
+  foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
 				       (LAcc x)..vee:=Lit (Intg #1)),
 				   Lit Null)"
-  ExtC_def  "ExtC  \\<equiv> (Ext,  (Some Base  , 
+  ExtC_def  "ExtC  == (Ext,  (Some Base  , 
 			     [(vee, PrimT Integer)], 
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
-  test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);; 
+  test_def "test == Expr(e::=NewC Ext);; 
                     Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -7,25 +7,25 @@
 val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
 
 Goalw [image_def]
-	"x \\<in> f``A \\<Longrightarrow> \\<exists>y. y \\<in> A \\<and>  x = f y";
+	"x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and>  x = f y";
 by(Auto_tac);
 qed "image_rev";
 
 fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
 
 val select_split = prove_goalw Prod.thy [split_def] 
-	"(\\<epsilon>(x,y). P x y) = (\\<epsilon>xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
+	"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
 	 
 
 val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
 	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
 val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
 	(fn _ => [Auto_tac]);
-val splitE2 = prove_goal Prod.thy "\\<lbrakk>Q (split P z); \\<And>x y. \\<lbrakk>z = (x, y); Q (P x y)\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
+val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
 	rtac (split_beta RS subst) 1,
 	rtac (hd prems) 1]);
-val splitE2' = prove_goal Prod.thy "\\<lbrakk>((\\<lambda>(x,y). P x y) z) w; \\<And>x y. \\<lbrakk>z = (x, y); (P x y) w\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
+val splitE2' = prove_goal Prod.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
 	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
 	res_inst_tac [("P1","P")] (split_beta RS subst) 1,
 	rtac (hd prems) 1]);
@@ -33,7 +33,7 @@
 
 fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
 
-val BallE = prove_goal thy "\\<lbrakk>Ball A P; x \\<notin> A \\<Longrightarrow> Q; P x \\<Longrightarrow> Q \\<rbrakk> \\<Longrightarrow> Q"
+val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q"
 	(fn prems => [rtac ballE 1, resolve_tac prems 1, 
 			eresolve_tac prems 1, eresolve_tac prems 1]);
 
@@ -43,7 +43,7 @@
 
 (* To HOL.ML *)
 
-val ex1_some_eq_trivial = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y" 
+val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y" 
 	(fn prems => [
 	cut_facts_tac prems 1,
 	rtac some_equality 1,
@@ -74,7 +74,7 @@
   asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
 
 val optionE = prove_goal thy 
-       "\\<lbrakk> opt = None \\<Longrightarrow> P;  \\<And>x. opt = Some x \\<Longrightarrow> P \\<rbrakk> \\<Longrightarrow> P" 
+       "[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" 
    (fn prems => [
 	case_tac "opt = None" 1,
 	 eresolve_tac prems 1,
@@ -87,7 +87,7 @@
 	 rotate_tac ~1  i   , asm_full_simp_tac HOL_basic_ss i];
 
 val option_map_SomeD = prove_goalw thy [option_map_def]
-	"\\<And>x. option_map f x = Some y \\<Longrightarrow> \\<exists>z. x = Some z \\<and> f z = y" (K [
+	"!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [
 	option_case_tac2 "x" 1,
 	 Auto_tac]);
 
@@ -120,19 +120,19 @@
 by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
 qed_spec_mp "unique_map_inj";
 
-Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
+Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
 by(etac unique_map_inj 1);
 by(rtac injI 1);
 by Auto_tac;
 qed "unique_map_Pair";
 
-Goal "\\<lbrakk>M = N; \\<And>x. x\\<in>N \\<Longrightarrow> f x = g x\\<rbrakk> \\<Longrightarrow> f``M = g``N";
+Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N";
 by(rtac set_ext 1);
 by(simp_tac (simpset() addsimps image_def::premises()) 1);
 qed "image_cong";
 
 val split_Pair_eq = prove_goal Prod.thy 
-"\\<And>X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A \\<Longrightarrow> y = Y" (K [
+"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
 	etac imageE 1,
 	split_all_tac 1,
 	auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
@@ -140,7 +140,7 @@
 
 (* More about Maps *)
 
-val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
+val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x ==> \
 \ t k = Some x |  t k = None \\<and>  s k = Some x" (fn prems => [
 	cut_facts_tac prems 1,
 	case_tac "\\<exists>x. t k = Some x" 1,
@@ -153,7 +153,7 @@
 
 Addsimps [fun_upd_same, fun_upd_other];
 
-Goal "unique xys \\<longrightarrow> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
+Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
 by(induct_tac "xys" 1);
  by(Simp_tac 1);
 by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
@@ -162,7 +162,7 @@
 val in_set_get = unique_map_of_Some_conv RS iffD2;
 val get_in_set = unique_map_of_Some_conv RS iffD1;
 
-Goal "(\\<forall>(x,y)\\<in>set l. P x y) \\<longrightarrow> (\\<forall>x. \\<forall>y. map_of l x = Some y \\<longrightarrow> P x y)";
+Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
 by(induct_tac "l" 1);
 by(ALLGOALS Simp_tac);
 by Safe_tac;
@@ -170,37 +170,37 @@
 bind_thm("Ball_set_table",result() RS mp);
 
 val table_mono = prove_goal thy 
-"unique l' \\<longrightarrow> (\\<forall>xy. (xy)\\<in>set l \\<longrightarrow> (xy)\\<in>set l') \\<longrightarrow>\
-\ (\\<forall>k y. map_of l k = Some y \\<longrightarrow> map_of l' k = Some y)" (fn _ => [
+"unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\
+\ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [
 	induct_tac "l" 1,
 	 Auto_tac,
  	 fast_tac (HOL_cs addSIs [in_set_get]) 1])
  RS mp RS mp RS spec RS spec RS mp;
 
-val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) \\<longrightarrow> \
+val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \
 \ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
 	induct_tac "t" 1,	
 	 ALLGOALS Simp_tac,
 	case_tac1 "k = fst a" 1,
 	 Auto_tac]) RS mp;
 val table_map_Some = prove_goal thy 
-"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \\<longrightarrow> \
+"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
 \map_of t (k, k') = Some x" (K [
 	induct_tac "t" 1,	
 	Auto_tac]) RS mp;
 
 
-val table_mapf_Some = prove_goal thy "\\<And>f. \\<forall>x y. f x = f y \\<longrightarrow> x = y \\<Longrightarrow> \
-\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) \\<longrightarrow> map_of t k = Some x" (K [
+val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \
+\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [
 	induct_tac "t" 1,	
 	Auto_tac]) RS mp;
 val table_mapf_SomeD = prove_goal thy 
-"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z \\<longrightarrow> (\\<exists>y. (k,y)\\<in>set t \\<and>  z = f y)"(K [
+"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and>  z = f y)"(K [
 	induct_tac "t" 1,	
 	Auto_tac]) RS mp;
 
 val table_mapf_Some2 = prove_goal thy 
-"\\<And>k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) \\<Longrightarrow> C = D \\<and> map_of t k = Some x" (K [
+"!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [
 	forward_tac [table_mapf_SomeD] 1,
 	Auto_tac,
 	rtac table_mapf_Some 1,
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -10,7 +10,7 @@
 
 constdefs
 
-  unique  :: "('a \\<times> 'b) list \\<Rightarrow> bool"
- "unique  \\<equiv> nodups \\<circ> map fst"
+  unique  :: "('a \\<times> 'b) list => bool"
+ "unique  == nodups \\<circ> map fst"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -9,16 +9,16 @@
 
 Addsimps [split_beta];
 
-Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C\\<rbrakk> \\<Longrightarrow> \
-\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)\\<Colon>\\<preceq>(G, lT)";
+Goal "[|h a = None; (h, l)::\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> \
+\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)::\\<preceq>(G, lT)";
 by( etac conforms_upd_obj 1);
 by(  rewtac oconf_def);
 by(  auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset()));
 qed "NewC_conforms";
 
 Goalw [cast_ok_def]
- "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v\\<rbrakk> \
-\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>Class D";
+ "[| wf_prog wf_mb G; G,h\\<turnstile>v::\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v|] \
+\ ==> G,h\\<turnstile>v::\\<preceq>Class D";
 by( case_tac1 "v = Null" 1);
 by(  Asm_full_simp_tac 1);
 by(  dtac widen_RefT 1);
@@ -28,9 +28,9 @@
 by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
 qed "Cast_conf";
 
-Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
-\    x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
-\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
+Goal "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\\<preceq>(G,lT); \
+\    x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
+\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\\<preceq>ft";
 by( dtac np_NoneD 1);
 by( etac conjE 1);
 by( mp_tac 1);
@@ -47,15 +47,15 @@
 qed "FAcc_type_sound";
 
 Goal
- "\\<lbrakk> wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
-\   (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
-\   (G, lT)\\<turnstile>aa\\<Colon>Class C; \
+ "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
+\   (G, lT)\\<turnstile>v::T'; G\\<turnstile>T'\\<preceq>ft; \
+\   (G, lT)\\<turnstile>aa::Class C; \
 \   field (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
-\   x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq> Class C; h'\\<le>|h; \
-\   (h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>x\\<Colon>\\<preceq>T'; np a' x' = None\\<rbrakk> \\<Longrightarrow> \
+\   x' = None --> G,h'\\<turnstile>a'::\\<preceq> Class C; h'\\<le>|h; \
+\   (h, l)::\\<preceq>(G, lT); G,h\\<turnstile>x::\\<preceq>T'; np a' x' = None|] ==> \
 \ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and>  \
-\ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)\\<Colon>\\<preceq>(G, lT) \\<and>  \
-\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x\\<Colon>\\<preceq>T'";
+\ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)::\\<preceq>(G, lT) \\<and>  \
+\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x::\\<preceq>T'";
 by( dtac np_NoneD 1);
 by( etac conjE 1);
 by( Asm_full_simp_tac 1);
@@ -91,11 +91,11 @@
 by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
 qed "FAss_type_sound";
 
-Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
+Goalw [wf_mhead_def] "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; \
  \ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; \
 \ length pTs' = length pns; nodups pns; \
 \ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
-\ \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[\\<Colon>\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
+\ |] ==> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[::\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
 by( Clarsimp_tac 1);
 by( rtac lconf_ext_list 1);
 by(    rtac (Ball_set_table RS lconf_init_vars) 1);
@@ -106,17 +106,17 @@
 qed "Call_lemma2";
 
 Goalw [wf_java_prog_def]
- "\\<lbrakk> wf_java_prog G; a' \\<noteq> Null; (h, l)\\<Colon>\\<preceq>(G, lT); \
+ "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); \
 \    max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
 \    list_all2 (conf G h) pvs pTsa;\
 \    (md, rT, pns, lvars, blk, res) = \
 \              the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
-\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> \
-\ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow>  h\\<le>|xi \\<and>  (xi, xl)\\<Colon>\\<preceq>(G, lT); \
-\ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
-\         xi\\<le>|h' \\<and> (h', xj)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)); \
-\ G,xh\\<turnstile>a'\\<Colon>\\<preceq> Class C \\<rbrakk> \\<Longrightarrow> \
-\ xc\\<le>|h' \\<and> (h', l)\\<Colon>\\<preceq>(G, lT) \\<and>  (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>rTa)";
+\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))::\\<preceq>(G, lT) --> \
+\ (G, lT)\\<turnstile>blk\\<surd> -->  h\\<le>|xi \\<and>  (xi, xl)::\\<preceq>(G, lT); \
+\ \\<forall>lT. (xi, xl)::\\<preceq>(G, lT) --> (\\<forall>T. (G, lT)\\<turnstile>res::T --> \
+\         xi\\<le>|h' \\<and> (h', xj)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>T)); \
+\ G,xh\\<turnstile>a'::\\<preceq> Class C |] ==> \
+\ xc\\<le>|h' \\<and> (h', l)::\\<preceq>(G, lT) \\<and>  (x' = None --> G,h'\\<turnstile>v::\\<preceq>rTa)";
 by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
 by( dtac (max_spec2appl_meths RS appl_methsD) 1);
 by( Clarify_tac 1);
@@ -139,9 +139,9 @@
 by( thin_tac "?E\\<turnstile>?blk\\<surd>" 1);
 by( etac conjE 1);
 by( EVERY'[dtac spec, mp_tac] 1);
-(*by( thin_tac "?E\\<Colon>\\<preceq>(G, pT')" 1);*)
+(*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
 by( EVERY'[dtac spec, mp_tac] 1);
-by( thin_tac "?E\\<turnstile>res\\<Colon>?rT" 1);
+by( thin_tac "?E\\<turnstile>res::?rT" 1);
 by( strip_tac1 1);
 by( rtac conjI 1);
 by(  fast_tac (HOL_cs addIs [hext_trans]) 1);
@@ -167,16 +167,16 @@
 val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
 	(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
 Goal
-"wf_java_prog G \\<Longrightarrow> \
-\ (G\\<turnstile>(x,(h,l)) -e  \\<succ>v  \\<rightarrow> (x', (h',l')) \\<longrightarrow> \
-\     (\\<forall>lT.    (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (\\<forall>T . (G,lT)\\<turnstile>e  \\<Colon> T \\<longrightarrow> \
-\     h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT) \\<and> (x'=None \\<longrightarrow> G,h'\\<turnstile>v  \\<Colon>\\<preceq> T )))) \\<and> \
-\ (G\\<turnstile>(x,(h,l)) -es[\\<succ>]vs\\<rightarrow> (x', (h',l')) \\<longrightarrow> \
-\     (\\<forall>lT.    (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (\\<forall>Ts. (G,lT)\\<turnstile>es[\\<Colon>]Ts \\<longrightarrow> \
-\     h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT) \\<and> (x'=None \\<longrightarrow> list_all2 (\\<lambda>v T. G,h'\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts)))) \\<and> \
-\ (G\\<turnstile>(x,(h,l)) -c       \\<rightarrow> (x', (h',l')) \\<longrightarrow> \
-\     (\\<forall>lT.    (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow>       (G,lT)\\<turnstile>c  \\<surd> \\<longrightarrow> \
-\     h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT)))";
+"wf_java_prog G ==> \
+\ (G\\<turnstile>(x,(h,l)) -e  \\<succ>v  -> (x', (h',l')) --> \
+\     (\\<forall>lT.    (h ,l )::\\<preceq>(G,lT) --> (\\<forall>T . (G,lT)\\<turnstile>e  :: T --> \
+\     h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> G,h'\\<turnstile>v  ::\\<preceq> T )))) \\<and> \
+\ (G\\<turnstile>(x,(h,l)) -es[\\<succ>]vs-> (x', (h',l')) --> \
+\     (\\<forall>lT.    (h ,l )::\\<preceq>(G,lT) --> (\\<forall>Ts. (G,lT)\\<turnstile>es[::]Ts --> \
+\     h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT) \\<and> (x'=None --> list_all2 (\\<lambda>v T. G,h'\\<turnstile>v::\\<preceq>T) vs Ts)))) \\<and> \
+\ (G\\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) --> \
+\     (\\<forall>lT.    (h ,l )::\\<preceq>(G,lT) -->       (G,lT)\\<turnstile>c  \\<surd> --> \
+\     h\\<le>|h' \\<and> (h',l')::\\<preceq>(G,lT)))";
 by( rtac eval_evals_exec.induct 1);
 by( rewtac c_hupd_def);
 
@@ -298,24 +298,24 @@
     THEN_ALL_NEW Asm_simp_tac) 1);
 qed "eval_evals_exec_type_sound";
 
-Goal "\\<And>E s s'. \
-\ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v \\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>T \\<rbrakk> \
-\ \\<Longrightarrow> s'\\<Colon>\\<preceq>E \\<and> (x'=None \\<longrightarrow> G,heap s'\\<turnstile>v\\<Colon>\\<preceq>T)";
+Goal "!!E s s'. \
+\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v -> (x',s'); s::\\<preceq>E; E\\<turnstile>e::T |] \
+\ ==> s'::\\<preceq>E \\<and> (x'=None --> G,heap s'\\<turnstile>v::\\<preceq>T)";
 by( split_all_tac 1);
 bd (eval_evals_exec_type_sound RS conjunct1 RS mp RS spec RS mp) 1;
 by Auto_tac;
 qed "eval_type_sound";
 
-Goal "\\<And>E s s'. \
-\ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -s0\\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>s0\\<surd> \\<rbrakk> \
-\ \\<Longrightarrow> s'\\<Colon>\\<preceq>E";
+Goal "!!E s s'. \
+\ [| G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -s0-> (x',s'); s::\\<preceq>E; E\\<turnstile>s0\\<surd> |] \
+\ ==> s'::\\<preceq>E";
 by( split_all_tac 1);
 bd (eval_evals_exec_type_sound RS conjunct2 RS conjunct2 RS mp RS spec RS mp) 1;
 by   Auto_tac;
 qed "exec_type_sound";
 
-Goal "\\<lbrakk>G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'\\<rightarrow> Norm s'; a' \\<noteq> Null;\
-\         s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>Class C; method (G,C) sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
+Goal "[|G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'-> Norm s'; a' \\<noteq> Null;\
+\         s::\\<preceq>E; E\\<turnstile>e::Class C; method (G,C) sig \\<noteq> None|] ==> \
 \ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
 by( datac eval_type_sound 4 1);
 by( not_None_tac 1);
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/State.ML
--- a/src/HOL/MicroJava/J/State.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/State.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -10,7 +10,7 @@
 Addsimps [obj_ty_def2];
 
 val new_AddrD = prove_goalw thy [new_Addr_def] 
-"\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
+"!!X. (a,x) = new_Addr h ==> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
 	asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
 	rtac someI 1,
 	rtac disjI2 1,
@@ -40,20 +40,20 @@
 Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
 
 val raise_if_SomeD = prove_goalw thy [raise_if_def] 
-	"raise_if c x y = Some z \\<longrightarrow> c \\<and>  Some z = Some x |  y = Some z" 
+	"raise_if c x y = Some z --> c \\<and>  Some z = Some x |  y = Some z" 
 (K [split_tac [split_if] 1,Auto_tac]) RS mp;
 
 val raise_if_NoneD = prove_goalw thy [raise_if_def] 
-	"raise_if c x y = None \\<longrightarrow> \\<not> c \\<and>  y = None"
+	"raise_if c x y = None --> \\<not> c \\<and>  y = None"
 (K [split_tac [split_if] 1,Auto_tac]) RS mp;
 
 
 val np_NoneD = (prove_goalw thy [np_def, raise_if_def] 
-	"np a' x' = None \\<longrightarrow> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
+	"np a' x' = None --> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
 	split_tac [split_if] 1,
 	Auto_tac ])) RS mp;
 val np_None = (prove_goalw thy [np_def, raise_if_def] 
-	"a' \\<noteq> Null \\<longrightarrow> np a' x' = x'" (fn _ => [
+	"a' \\<noteq> Null --> np a' x' = x'" (fn _ => [
 	split_tac [split_if] 1,
 	Auto_tac ])) RS mp;
 val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -15,11 +15,11 @@
 
 constdefs
 
-  obj_ty	:: "obj \\<Rightarrow> ty"
- "obj_ty obj  \\<equiv> Class (fst obj)"
+  obj_ty	:: "obj => ty"
+ "obj_ty obj  == Class (fst obj)"
 
-  init_vars	:: "('a \\<times> ty) list \\<Rightarrow> ('a \\<leadsto> val)"
- "init_vars	\\<equiv> map_of o map (\\<lambda>(n,T). (n,default_val T))"
+  init_vars	:: "('a \\<times> ty) list => ('a \\<leadsto> val)"
+ "init_vars	== map_of o map (\\<lambda>(n,T). (n,default_val T))"
   
 datatype xcpt		(* exceptions *)
 	= NullPointer
@@ -37,9 +37,9 @@
 	 = "xcpt option \\<times> state"
 
 syntax
-  heap		:: "state \\<Rightarrow> aheap"
-  locals	:: "state \\<Rightarrow> locals"
-  Norm		:: "state \\<Rightarrow> xstate"
+  heap		:: "state => aheap"
+  locals	:: "state => locals"
+  Norm		:: "state => xstate"
 
 translations
   "heap"	=> "fst"
@@ -48,19 +48,19 @@
 
 constdefs
 
-  new_Addr	:: "aheap \\<Rightarrow> loc \\<times> xcpt option"
- "new_Addr h \\<equiv> \\<epsilon>(a,x). (h a = None \\<and>  x = None) |  x = Some OutOfMemory"
+  new_Addr	:: "aheap => loc \\<times> xcpt option"
+ "new_Addr h == SOME (a,x). (h a = None \\<and>  x = None) |  x = Some OutOfMemory"
 
-  raise_if	:: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option"
- "raise_if c x xo \\<equiv> if c \\<and>  (xo = None) then Some x else xo"
+  raise_if	:: "bool => xcpt => xcpt option => xcpt option"
+ "raise_if c x xo == if c \\<and>  (xo = None) then Some x else xo"
 
-  np		:: "val \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option"
- "np v \\<equiv> raise_if (v = Null) NullPointer"
+  np		:: "val => xcpt option => xcpt option"
+ "np v == raise_if (v = Null) NullPointer"
 
-  c_hupd	:: "aheap \\<Rightarrow> xstate \\<Rightarrow> xstate"
- "c_hupd h'\\<equiv> \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
+  c_hupd	:: "aheap => xstate => xstate"
+ "c_hupd h'== \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
 
-  cast_ok	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
- "cast_ok G C h v \\<equiv> v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
+  cast_ok	:: "'c prog => cname => aheap => val => bool"
+ "cast_ok G C h v == v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -16,7 +16,7 @@
 	| Lit	val		   (* literal value, also references *)
         | BinOp binop  expr expr   (* binary operation *)
 	| LAcc vname		   (* local (incl. parameter) access *)
-	| LAss vname expr          (* local assign *) ("_\\<Colon>=_"  [      90,90]90)
+	| LAss vname expr          (* local assign *) ("_::=_"  [      90,90]90)
 	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
 	| FAss cname expr vname 
 	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Type.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -31,7 +31,7 @@
 
 syntax
          NT     :: "          ty"
-	 Class	:: "cname  \\<Rightarrow> ty"
+	 Class	:: "cname  => ty"
 translations
 	"NT"      == "RefT   NullT"
 	"Class C" == "RefT (ClassT C)"
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -4,11 +4,11 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-val subcls1D = prove_goalw thy [subcls1_def] "\\<And>G. G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> \
+val subcls1D = prove_goalw thy [subcls1_def] "!!G. G\\<turnstile>C\\<prec>C1D ==> \
 \ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]);
 
 val subcls1I = prove_goalw  thy [subcls1_def] 
-"\\<And>G. \\<lbrakk> class G C = Some (Some D,rest) \\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
+"!!G. [| class G C = Some (Some D,rest) |] ==> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
 
 val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def]  "subcls1 G = \
 \ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
@@ -32,7 +32,7 @@
 	auto_tac (claset() addDs lemmata, simpset())]);
 
 
-Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ \\<Longrightarrow> is_class G C";
+Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
 by(etac trancl_trans_induct 1);
 by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
 qed "subcls_is_class";
@@ -81,16 +81,16 @@
 qed "widen_PrimT_RefT";
 AddIffs [widen_PrimT_RefT];
 
-val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t" 
-	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
+val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t" 
+	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)"];
 bind_thm ("widen_RefT", widen_RefT);
 
-val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
-	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
+val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t" 
+	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)"];
 bind_thm ("widen_RefT2", widen_RefT2);
 
-val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D"
- [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> (\\<exists>D. T=Class D)"];
+val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D"
+ [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)"];
 bind_thm ("widen_Class", widen_Class);
 
 Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; 
@@ -108,7 +108,7 @@
 qed "widen_Class_Class";
 AddIffs [widen_Class_Class];
 
-Goal "G\\<turnstile>S\\<preceq>U \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
+Goal "G\\<turnstile>S\\<preceq>U ==> \\<forall>T. G\\<turnstile>U\\<preceq>T --> G\\<turnstile>S\\<preceq>T";
 by( etac widen.induct 1);
 by   Safe_tac;
 by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -9,15 +9,15 @@
 TypeRel = Decl +
 
 consts
-  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* subclass *)
-  widen 	:: "'c prog \\<Rightarrow> (ty    \\<times> ty   ) set"  (* widening *)
-  cast		:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* casting *)
+  subcls1	:: "'c prog => (cname \\<times> cname) set"  (* subclass *)
+  widen 	:: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
+  cast		:: "'c prog => (cname \\<times> cname) set"  (* casting *)
 
 syntax
-  subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
-  subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
-  widen		:: "'c prog \\<Rightarrow> [ty   , ty   ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
-  cast		:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
+  subcls1	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
+  subcls	:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
+  widen		:: "'c prog => [ty   , ty   ] => bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
+  cast		:: "'c prog => [cname, cname] => bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
 
 translations
   	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
@@ -28,23 +28,23 @@
 defs
 
   (* direct subclass, cf. 8.1.3 *)
-  subcls1_def	"subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
+  subcls1_def	"subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
   
 consts
 
-  method	:: "'c prog \\<times> cname \\<Rightarrow> ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
-  field	:: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
-  fields	:: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times>  ty) list"
+  method	:: "'c prog \\<times> cname => ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
+  field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
+  fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
 
 constdefs       (* auxiliary relations for recursive definitions below *)
 
   subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
- "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
+ "subcls1_rel == {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
 
 (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
 recdef method "subcls1_rel"
- "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
-                   | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> 
+ "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
+                   | Some (sc,fs,ms) => (case sc of None => empty | Some D => 
                                            if is_class G D then method (G,D) 
                                                            else arbitrary) \\<oplus>
                                            map_of (map (\\<lambda>(s,  m ). 
@@ -53,25 +53,25 @@
 
 (* list of fields of a class, including inherited and hidden ones *)
 recdef fields  "subcls1_rel"
- "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> arbitrary
-                   | Some (sc,fs,ms) \\<Rightarrow> map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
-                                           (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> 
+ "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
+                   | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
+                                           (case sc of None => [] | Some D => 
                                            if is_class G D then fields (G,D) 
                                                            else arbitrary))
                   else arbitrary)"
 defs
 
-  field_def "field \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+  field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
 
 inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
 			     i.e. sort of syntactic subtyping *)
   refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
-  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
+  subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D"
   null	             "G\\<turnstile>     NT \\<preceq> RefT R"
 
 inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
                          (* left out casts on primitve types    *)
-  widen	 "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
-  subcls "G\\<turnstile>D\\<preceq>C C \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
+  widen	 "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D"
+  subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/Value.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -22,9 +22,9 @@
 translations "val" <= (type) "val_"
 
 consts
-  the_Bool	:: "val \\<Rightarrow> bool"
-  the_Intg	:: "val \\<Rightarrow> int"
-  the_Addr	:: "val \\<Rightarrow> loc"
+  the_Bool	:: "val => bool"
+  the_Intg	:: "val => int"
+  the_Addr	:: "val => loc"
 
 primrec
  "the_Bool (Bool b) = b"
@@ -36,8 +36,8 @@
  "the_Addr (Addr a) = a"
 
 consts
-  defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
-  default_val	:: "ty \\<Rightarrow> val"		(* default value for all types *)
+  defpval	:: "prim_ty => val"	(* default value for primitive types *)
+  default_val	:: "ty => val"		(* default value for all types *)
 
 primrec
 	"defpval Void    = Unit"
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/WellForm.ML
--- a/src/HOL/MicroJava/J/WellForm.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -5,22 +5,22 @@
 *)
 
 val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
- "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wf_cdecl wf_mb G (C,c)" (K [
+ "!!X. [|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)" (K [
 	Asm_full_simp_tac 1,
 	fast_tac (set_cs addDs [get_in_set]) 1]);
 
 val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
-	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
+	"!!X. wf_prog wf_mb G ==> class G Object = Some (None, [], [])" (K [
 	safe_tac set_cs,
 	dtac in_set_get 1,
 	 Auto_tac]);
 Addsimps [class_Object];
 
 val is_class_Object = prove_goalw thy [is_class_def] 
-	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
+	"!!X. wf_prog wf_mb G ==> is_class G Object" (K [Asm_simp_tac 1]);
 Addsimps [is_class_Object];
 
-Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
+Goal "[|G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G|] ==> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
 by( forward_tac [r_into_trancl] 1);
 by( dtac subcls1D 1);
 by( strip_tac1 1);
@@ -31,26 +31,26 @@
 qed "subcls1_wfD";
 
 val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] 
-"\\<And>X. \\<lbrakk>wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
+"!!X. [|wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object|] ==> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
 	pair_tac "r" 1,
 	asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
 
-Goal "\\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> \\<not>(D,C)\\<in>(subcls1 G)^+";
+Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> \\<not>(D,C)\\<in>(subcls1 G)^+";
 by(etac tranclE 1);
 by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
 qed "subcls_asym";
 
-val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
+val subcls_irrefl = prove_goal thy "!!X. [|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D" (K [
 	etac trancl_trans_induct 1,
 	 fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
 	fast_tac (HOL_cs addDs [subcls_asym]) 1]);
 
 val acyclic_subcls1 = prove_goalw thy [acyclic_def] 
-	"\\<And>X. wf_prog wf_mb G \\<Longrightarrow> acyclic (subcls1 G)" (K [
+	"!!X. wf_prog wf_mb G ==> acyclic (subcls1 G)" (K [
 	strip_tac1 1,
 	fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
 
-val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
+val wf_subcls1 = prove_goal thy "!!X. wf_prog wf_mb G ==> wf ((subcls1 G)^-1)" (K [
 	rtac finite_acyclic_wf 1,
 	 stac finite_converse 1,
 	 rtac finite_subcls1 1,
@@ -58,7 +58,7 @@
 	etac acyclic_subcls1 1]);
 
 val major::prems = goal thy
-  "\\<lbrakk>wf_prog wf_mb G; \\<And>C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
+  "[|wf_prog wf_mb G; !!C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C";
 by(cut_facts_tac [major RS wf_subcls1] 1);
 by(dtac wf_trancl 1);
 by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
@@ -67,10 +67,10 @@
 by(Auto_tac);
 qed "subcls_induct";
 
-val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wf_mb G; P Object; \
-\\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
-\   wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
-\ \\<rbrakk> \\<Longrightarrow> P C";
+val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
+\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
+\   wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
+\ |] ==> P C";
 by( cut_facts_tac prems 1);
 by( rtac impE 1);
 by(   atac 2);
@@ -95,18 +95,18 @@
 by( etac subcls1I 1);
 qed "subcls1_induct";
 
-Goal "\\<lbrakk>wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) \\<longrightarrow> is_class G D\\<rbrakk> \\<Longrightarrow> method (G,C) = \
-\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
-\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
+Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) --> is_class G D|] ==> method (G,C) = \
+\ (case class G C of None => empty | Some (sc,fs,ms) => \
+\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
 by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
 by( asm_simp_tac (simpset() addsplits[option.split]) 1);
 auto();
 qed "method_rec_lemma";
 
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
-\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
-\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
+Goal "wf_prog wf_mb G ==> method (G,C) = \
+\ (case class G C of None => empty | Some (sc,fs,ms) => \
+\ (case sc of None => empty | Some D => method (G,D)) \\<oplus> \
 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
 by(rtac method_rec_lemma 1);
 by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] 
@@ -119,16 +119,16 @@
 by( Asm_full_simp_tac 1);
 qed "method_rec";
 
-Goal "\\<lbrakk>wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C \\<longrightarrow> is_class G C\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
+Goal "[|wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C --> is_class G C|] ==> fields (G,C) = \
 \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
+\ (case sc of None => [] | Some D => fields (G,D))";
 by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
 by( asm_simp_tac (simpset() addsplits[option.split]) 1);
 qed "fields_rec_lemma";
 
-Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
+Goal "[|class G C = Some (sc,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
 \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
+\ (case sc of None => [] | Some D => fields (G,D))";
 by(rtac fields_rec_lemma 1);
 by(   asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
 ba  1;
@@ -142,16 +142,16 @@
 by( Asm_full_simp_tac 1);
 qed "fields_rec";
 
-val method_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> method (G,Object) = empty"
+val method_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> method (G,Object) = empty"
 	(K [stac method_rec 1,Auto_tac]);
-val fields_Object = prove_goal thy "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> fields (G,Object) = []"(K [
+val fields_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> fields (G,Object) = []"(K [
 	stac fields_rec 1,Auto_tac]);
 Addsimps [method_Object, fields_Object];
 val field_Object = prove_goalw thy [field_def]
- "\\<And>X. wf_prog wf_mb G \\<Longrightarrow> field (G,Object) = empty" (K [Asm_simp_tac 1]);
+ "!!X. wf_prog wf_mb G ==> field (G,Object) = empty" (K [Asm_simp_tac 1]);
 Addsimps [field_Object];
 
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<preceq>C Object";
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> G\\<turnstile>C\\<preceq>C Object";
 by(etac subcls1_induct 1);
 by(  atac 1);
 by( Fast_tac 1);
@@ -160,18 +160,18 @@
 qed "subcls_C_Object";
 
 val is_type_rTI = prove_goalw thy [wf_mhead_def]
-	"\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
+	"!!sig. wf_mhead G sig rT ==> is_type G rT"
 	(K [split_all_tac 1, Auto_tac]);
 
-Goal "\\<lbrakk>(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
-\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))";
+Goal "[|(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G|] ==> \
+\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
 by(etac trancl_trans_induct 1);
 by( safe_tac (HOL_cs addSDs [subcls1D]));
 by(stac fields_rec 1);
 by(  Auto_tac);
 qed_spec_mp "fields_mono";
 
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
 \ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
 by( etac subcls1_induct 1);
 by(   atac 1);
@@ -193,7 +193,7 @@
 by( Asm_full_simp_tac 1);
 qed "widen_fields_defpl'";
 
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
+Goal "[|is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))|] ==> \
 \ G\\<turnstile>C\\<preceq>C fd";
 by( datac widen_fields_defpl' 1 1);
 (*###################*)
@@ -202,7 +202,7 @@
 qed "widen_fields_defpl";
 
 
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))";
 by( etac subcls1_induct 1);
 by(   atac 1);
 by(  safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
@@ -226,7 +226,7 @@
 qed "unique_fields";
 
 Goal
-"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
+"[|wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft|] ==> \
 \                          map_of (fields (G,C')) f = Some ft";
 by( dtac rtranclD 1);
 by( Auto_tac);
@@ -240,17 +240,17 @@
 
 
 val cfs_fields_lemma = prove_goalw thy [field_def] 
-"\\<And>X. field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
+"!!X. field (G,C) fn = Some (fd, fT) ==> map_of(fields (G,C)) (fn, fd) = Some fT"
 (K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
 
-val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>field (G,C) fn = Some (fd, fT);\
-\  G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
+val widen_cfs_fields = prove_goal thy "!!X. [|field (G,C) fn = Some (fd, fT);\
+\  G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G|] ==> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
 fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
 bind_thm ("widen_cfs_fields",widen_cfs_fields);
 
 
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) sig = Some (md,mh,m)\
-\  \\<longrightarrow> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
+Goal "wf_prog wf_mb G ==> method (G,C) sig = Some (md,mh,m)\
+\  --> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
 by( case_tac "is_class G C" 1);
 by(  forw_inst_tac [("C","C")] method_rec 2);
 by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
@@ -264,7 +264,7 @@
 by( Asm_full_simp_tac 1);
 by( dtac override_SomeD 1);
 by( etac disjE 1);
-by(  thin_tac "?P \\<longrightarrow> ?Q" 1);
+by(  thin_tac "?P --> ?Q" 1);
 by(  Clarify_tac 2);
 by(  rtac rtrancl_trans 2);
 by(   atac 3);
@@ -277,8 +277,8 @@
 by( Asm_full_simp_tac 1);
 qed_spec_mp "method_wf_mdecl";
 
-Goal "\\<lbrakk>G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
-\  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
+Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
+\  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->\
 \ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
 by( dtac rtranclD 1);
 by( etac disjE 1);
@@ -312,15 +312,15 @@
 
 
 Goal
- "\\<lbrakk> G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
-\    method (G,D) sig = Some (md, rT, b) \\<rbrakk> \
-\ \\<Longrightarrow> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+ "[| G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
+\    method (G,D) sig = Some (md, rT, b) |] \
+\ ==> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
 by(auto_tac (claset() addDs [subcls_widen_methd,method_wf_mdecl],
              simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
 qed "subtype_widen_methd";
 
 
-Goal "wf_prog wf_mb G \\<Longrightarrow> \\<forall>D. method (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
+Goal "wf_prog wf_mb G ==> \\<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
 by( case_tac "is_class G C" 1);
 by(  forw_inst_tac [("C","C")] method_rec 2);
 by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
@@ -341,7 +341,7 @@
 qed_spec_mp "method_in_md";
 
 
-Goal "\\<lbrakk>is_class G C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
 \ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
 by( etac subcls1_induct 1);
 by(   atac 1);
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -20,28 +20,28 @@
 
 constdefs
 
- wf_fdecl	:: "'c prog \\<Rightarrow>          fdecl \\<Rightarrow> bool"
-"wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft"
+ wf_fdecl	:: "'c prog =>          fdecl => bool"
+"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
 
- wf_mhead	:: "'c prog \\<Rightarrow> sig   \\<Rightarrow> ty \\<Rightarrow> bool"
-"wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
+ wf_mhead	:: "'c prog => sig   => ty => bool"
+"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
 
- wf_mdecl	:: "'c wf_mb \\<Rightarrow> 'c wf_mb"
-"wf_mdecl wf_mb G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
+ wf_mdecl	:: "'c wf_mb => 'c wf_mb"
+"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
 
-  wf_cdecl	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
-"wf_cdecl wf_mb G \\<equiv>
+  wf_cdecl	:: "'c wf_mb => 'c prog => 'c cdecl => bool"
+"wf_cdecl wf_mb G ==
    \\<lambda>(C,(sc,fs,ms)).
 	(\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
 	(\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
-	(case sc of None \\<Rightarrow> C = Object
-         | Some D \\<Rightarrow>
+	(case sc of None => C = Object
+         | Some D =>
              is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
              (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
-                 method(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+                 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
 
- wf_prog	:: "'c wf_mb \\<Rightarrow> 'c prog \\<Rightarrow> bool"
-"wf_prog wf_mb G \\<equiv>
+ wf_prog	:: "'c wf_mb => 'c prog => bool"
+"wf_prog wf_mb G ==
    let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -5,15 +5,15 @@
 *)
 
 Goal
-"\\<lbrakk> method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C\\<rbrakk>\
-\ \\<Longrightarrow> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
+"[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\\<turnstile>T''\\<preceq>C C|]\
+\ ==> \\<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
 by( dtac subcls_widen_methd 1);
 by   Auto_tac;
 qed "widen_methd";
 
 
 Goal
-"\\<lbrakk>method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> \
+"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G|] ==> \
 \ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
 \ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
 by( datac widen_methd 2 1);
@@ -25,25 +25,25 @@
 qed "Call_lemma";
 
 
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,Object) sig = None";
+Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
 by (Asm_simp_tac 1);
 qed "method_Object";
 Addsimps [method_Object];
 
 Goalw [max_spec_def] 
-  "x \\<in> max_spec G C sig \\<Longrightarrow> x \\<in> appl_methds G C sig";
+  "x \\<in> max_spec G C sig ==> x \\<in> appl_methds G C sig";
 by (Fast_tac 1);
 qed"max_spec2appl_meths";
 
 Goalw [appl_methds_def] 
-"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) \\<Longrightarrow> \
+"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) ==> \
 \ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \
 \ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'";
 by (Fast_tac 1);
 qed "appl_methsD";
 
 val is_type_typeof = prove_goal thy 
-	"(\\<forall>a. v \\<noteq> Addr a) \\<longrightarrow> (\\<exists>T. typeof t v = Some T \\<and>  is_type G T)" (K [
+	"(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and>  is_type G T)" (K [
 	rtac val_.induct 1,
 	    Fast_tac 5,
 	   ALLGOALS Simp_tac]) RS mp;
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -24,8 +24,8 @@
 
 syntax
 
-  prg		:: "'c env \\<Rightarrow> 'c prog"
-  localT	:: "'c env \\<Rightarrow> (vname \\<leadsto> ty)"
+  prg		:: "'c env => 'c prog"
+  localT	:: "'c env => (vname \\<leadsto> ty)"
 
 translations	
 
@@ -34,29 +34,29 @@
 
 consts
 
-  more_spec	:: "'c prog \\<Rightarrow> (ty \\<times> 'x) \\<times> ty list \\<Rightarrow>
-		               (ty \\<times> 'x) \\<times> ty list \\<Rightarrow> bool"
-  appl_methds	:: "'c prog \\<Rightarrow>  cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
-  max_spec	:: "'c prog \\<Rightarrow>  cname \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
+  more_spec	:: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
+		               (ty \\<times> 'x) \\<times> ty list => bool"
+  appl_methds	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+  max_spec	:: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
 
 defs
 
-  more_spec_def	  "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
+  more_spec_def	  "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
 		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
   
   (* applicable methods, cf. 15.11.2.1 *)
-  appl_methds_def "appl_methds G C \\<equiv> \\<lambda>(mn, pTs).
+  appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
 		                 {((Class md,rT),pTs') |md rT mb pTs'.
 		                  method (G,C)  (mn, pTs') = Some (md,rT,mb) \\<and>
 		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
 
   (* maximally specific methods, cf. 15.11.2.2 *)
-   max_spec_def	  "max_spec G C sig \\<equiv> {m. m \\<in>appl_methds G C sig \\<and> 
+   max_spec_def	  "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and> 
 				          (\\<forall>m'\\<in>appl_methds G C sig.
-				                   more_spec G m' m \\<longrightarrow> m' = m)}"
+				                   more_spec G m' m --> m' = m)}"
 consts
 
-  typeof :: "(loc \\<Rightarrow> ty option) \\<Rightarrow> val \\<Rightarrow> ty option"
+  typeof :: "(loc => ty option) => val => ty option"
 
 primrec
 	"typeof dt  Unit    = Some (PrimT Void)"
@@ -71,19 +71,19 @@
 
 consts
 
-  ty_expr :: "java_mb env \\<Rightarrow> (expr      \\<times> ty     ) set"
-  ty_exprs:: "java_mb env \\<Rightarrow> (expr list \\<times> ty list) set"
-  wt_stmt :: "java_mb env \\<Rightarrow>  stmt                 set"
+  ty_expr :: "java_mb env => (expr      \\<times> ty     ) set"
+  ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
+  wt_stmt :: "java_mb env =>  stmt                 set"
 
 syntax
 
-ty_expr :: "java_mb env \\<Rightarrow> [expr     , ty     ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_"  [51,51,51]50)
-ty_exprs:: "java_mb env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
-wt_stmt :: "java_mb env \\<Rightarrow>  stmt                \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51   ]50)
+ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_\\<turnstile>_::_"  [51,51,51]50)
+ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_\\<turnstile>_[::]_"[51,51,51]50)
+wt_stmt :: "java_mb env =>  stmt                => bool" ("_\\<turnstile>_ \\<surd>" [51,51   ]50)
 
 translations
-	"E\\<turnstile>e \\<Colon> T" == "(e,T) \\<in> ty_expr  E"
-	"E\\<turnstile>e[\\<Colon>]T" == "(e,T) \\<in> ty_exprs E"
+	"E\\<turnstile>e :: T" == "(e,T) \\<in> ty_expr  E"
+	"E\\<turnstile>e[::]T" == "(e,T) \\<in> ty_exprs E"
 	"E\\<turnstile>c \\<surd>"    == "c     \\<in> wt_stmt  E"
   
 inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
@@ -91,98 +91,98 @@
 (* well-typed expressions *)
 
   (* cf. 15.8 *)
-  NewC	"\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>NewC C\\<Colon>Class C"
+  NewC	"[|is_class (prg E) C|] ==>
+						 E\\<turnstile>NewC C::Class C"
 
   (* cf. 15.15 *)
-  Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>Class C;
-	  prg E\\<turnstile>C\\<preceq>? D\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>Cast D e\\<Colon>Class D"
+  Cast	"[|E\\<turnstile>e::Class C;
+	  prg E\\<turnstile>C\\<preceq>? D|] ==>
+						 E\\<turnstile>Cast D e::Class D"
 
   (* cf. 15.7.1 *)
-  Lit	"\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>Lit x\\<Colon>T"
+  Lit	"[|typeof (\\<lambda>v. None) x = Some T|] ==>
+						 E\\<turnstile>Lit x::T"
 
   
   (* cf. 15.13.1 *)
-  LAcc	"\\<lbrakk>localT E v = Some T; is_type (prg E) T\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>LAcc v\\<Colon>T"
+  LAcc	"[|localT E v = Some T; is_type (prg E) T|] ==>
+						 E\\<turnstile>LAcc v::T"
 
-  BinOp "\\<lbrakk>E\\<turnstile>e1\\<Colon>T;
-	  E\\<turnstile>e2\\<Colon>T;
+  BinOp "[|E\\<turnstile>e1::T;
+	  E\\<turnstile>e2::T;
 	  if bop = Eq then T' = PrimT Boolean
-	              else T' = T \\<and> T = PrimT Integer\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>BinOp bop e1 e2\\<Colon>T'"
+	              else T' = T \\<and> T = PrimT Integer|] ==>
+						 E\\<turnstile>BinOp bop e1 e2::T'"
 
   (* cf. 15.25, 15.25.1 *)
-  LAss  "\\<lbrakk>E\\<turnstile>LAcc v\\<Colon>T;
-	  E\\<turnstile>e\\<Colon>T';
-	  prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>v\\<Colon>=e\\<Colon>T'"
+  LAss  "[|E\\<turnstile>LAcc v::T;
+	  E\\<turnstile>e::T';
+	  prg E\\<turnstile>T'\\<preceq>T|] ==>
+						 E\\<turnstile>v::=e::T'"
 
   (* cf. 15.10.1 *)
-  FAcc	"\\<lbrakk>E\\<turnstile>a\\<Colon>Class C; 
-	  field (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>{fd}a..fn\\<Colon>fT"
+  FAcc	"[|E\\<turnstile>a::Class C; 
+	  field (prg E,C) fn = Some (fd,fT)|] ==>
+						 E\\<turnstile>{fd}a..fn::fT"
 
   (* cf. 15.25, 15.25.1 *)
-  FAss  "\\<lbrakk>E\\<turnstile>{fd}a..fn\\<Colon>T;
-	  E\\<turnstile>v       \\<Colon>T';
-	  prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
-					 	 E\\<turnstile>{fd}a..fn:=v\\<Colon>T'"
+  FAss  "[|E\\<turnstile>{fd}a..fn::T;
+	  E\\<turnstile>v       ::T';
+	  prg E\\<turnstile>T'\\<preceq>T|] ==>
+					 	 E\\<turnstile>{fd}a..fn:=v::T'"
 
 
   (* cf. 15.11.1, 15.11.2, 15.11.3 *)
-  Call	"\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
-	  E\\<turnstile>ps[\\<Colon>]pTs;
-	  max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>a..mn({pTs'}ps)\\<Colon>rT"
+  Call	"[|E\\<turnstile>a::Class C;
+	  E\\<turnstile>ps[::]pTs;
+	  max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}|] ==>
+						 E\\<turnstile>a..mn({pTs'}ps)::rT"
 
 (* well-typed expression lists *)
 
   (* cf. 15.11.??? *)
-  Nil						"E\\<turnstile>[][\\<Colon>][]"
+  Nil						"E\\<turnstile>[][::][]"
 
   (* cf. 15.11.??? *)
-  Cons	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
-	   E\\<turnstile>es[\\<Colon>]Ts\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>e#es[\\<Colon>]T#Ts"
+  Cons	"[|E\\<turnstile>e::T;
+	   E\\<turnstile>es[::]Ts|] ==>
+						 E\\<turnstile>e#es[::]T#Ts"
 
 (* well-typed statements *)
 
   Skip					"E\\<turnstile>Skip\\<surd>"
 
-  Expr	"\\<lbrakk>E\\<turnstile>e\\<Colon>T\\<rbrakk> \\<Longrightarrow>
+  Expr	"[|E\\<turnstile>e::T|] ==>
 					 E\\<turnstile>Expr e\\<surd>"
 
-  Comp	"\\<lbrakk>E\\<turnstile>s1\\<surd>; 
-	  E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
+  Comp	"[|E\\<turnstile>s1\\<surd>; 
+	  E\\<turnstile>s2\\<surd>|] ==>
 					 E\\<turnstile>s1;; s2\\<surd>"
 
   (* cf. 14.8 *)
-  Cond	"\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
+  Cond	"[|E\\<turnstile>e::PrimT Boolean;
 	  E\\<turnstile>s1\\<surd>;
-	  E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
+	  E\\<turnstile>s2\\<surd>|] ==>
 					 E\\<turnstile>If(e) s1 Else s2\\<surd>"
 
   (* cf. 14.10 *)
-  Loop "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
-	 E\\<turnstile>s\\<surd>\\<rbrakk> \\<Longrightarrow>
+  Loop "[|E\\<turnstile>e::PrimT Boolean;
+	 E\\<turnstile>s\\<surd>|] ==>
 					 E\\<turnstile>While(e) s\\<surd>"
 
 constdefs
 
  wf_java_mdecl :: java_mb prog => cname => java_mb mdecl => bool
-"wf_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
+"wf_java_mdecl G C == \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
 	length pTs = length pns \\<and>
 	nodups pns \\<and>
 	unique lvars \\<and>
 	(\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
 	(\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
 	(let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
-	 E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"
+	 E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res::T \\<and> G\\<turnstile>T\\<preceq>rT))"
 
  wf_java_prog :: java_mb prog => bool
-"wf_java_prog G \\<equiv> wf_prog wf_java_mdecl G"
+"wf_java_prog G == wf_prog wf_java_mdecl G"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/JVM/JVMExec.thy
--- a/src/HOL/MicroJava/JVM/JVMExec.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -9,7 +9,7 @@
 JVMExec = JVMExecInstr + 
 
 consts
- exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
+ exec :: "jvm_prog \\<times> jvm_state => jvm_state option"
 
 (** exec is not recursive. recdef is just used for pattern matching **)
 recdef exec "{}"
@@ -25,7 +25,7 @@
 
 
 constdefs
- exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool"  ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
- "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
+ exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"  ("_ \\<turnstile> _ -jvm-> _" [61,61,61]60)
+ "G \\<turnstile> s -jvm-> t == (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
 
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/JVM/JVMExecInstr.thy
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -9,7 +9,7 @@
 JVMExecInstr = JVMInstructions + JVMState +
 
 consts
-exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] \\<Rightarrow> jvm_state"
+exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars, cname, sig, p_count, frame list] => jvm_state"
 primrec
  "exec_instr (Load idx) G hp stk vars Cl sig pc frs = 
       (None, hp, ((vars ! idx) # stk, vars, Cl, sig, pc+1)#frs)"
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/JVM/JVMState.thy
--- a/src/HOL/MicroJava/JVM/JVMState.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -32,8 +32,8 @@
 (** exceptions **)
 
 constdefs
- raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
-"raise_xcpt c x \\<equiv> (if c then Some x else None)"
+ raise_xcpt :: "bool => xcpt => xcpt option"
+"raise_xcpt c x == (if c then Some x else None)"
 
 (** runtime state **)
 
@@ -45,6 +45,6 @@
 (** dynamic method lookup **)
 
 constdefs
- dyn_class	:: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
-"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
+ dyn_class	:: "'code prog \\<times> sig \\<times> cname => cname"
+"dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
 end
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/JVM/Store.ML
--- a/src/HOL/MicroJava/JVM/Store.ML	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.ML	Thu Sep 21 10:42:49 2000 +0200
@@ -5,6 +5,6 @@
 *)
 
 Goalw [newref_def]
- "hp x = None \\<longrightarrow> hp (newref hp) = None";
+ "hp x = None --> hp (newref hp) = None";
 by (fast_tac (claset() addIs [someI2_ex] addss (simpset())) 1);
 qed_spec_mp "newref_None";
diff -r 30693ebd16ae -r 7164dc0d24d8 src/HOL/MicroJava/JVM/Store.thy
--- a/src/HOL/MicroJava/JVM/Store.thy	Wed Sep 20 21:20:41 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.thy	Thu Sep 21 10:42:49 2000 +0200
@@ -12,7 +12,7 @@
 Store = Conform +  
 
 constdefs
- newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
- "newref s \\<equiv> \\<epsilon>v. s v = None"
+ newref :: "('a \\<leadsto> 'b) => 'a"
+ "newref s == SOME v. s v = None"
 
 end