diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -11,10 +11,10 @@
 
 constdefs
 
-dynamic_wt :: "'s ord => 's err step_type => 's err list => bool"
+dynamic_wt :: "'s ord \<Rightarrow> 's err step_type \<Rightarrow> 's err list \<Rightarrow> bool"
 "dynamic_wt r step ts == wt_step (Err.le r) Err step ts"
 
-static_wt :: "'s ord => (nat => 's => bool) => 's step_type => 's list => bool"
+static_wt :: "'s ord \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
 "static_wt r app step ts == 
   \<forall>p < size ts. app p (ts!p) \<and> (\<forall>(q,t) \<in> set (step p (ts!p)). t <=_r ts!q)"
 
@@ -28,14 +28,14 @@
 "err_step app step p t == case t of Err \<Rightarrow> map_err (step p arbitrary) | OK t' \<Rightarrow> 
   if app p t' then map_snd OK (step p t') else map_err (step p t')"
 
-non_empty :: "'s step_type => bool"
+non_empty :: "'s step_type \<Rightarrow> bool"
 "non_empty step == \<forall>p t. step p t \<noteq> []"
 
 
 lemmas err_step_defs = err_step_def map_snd_def map_err_def
 
 lemma non_emptyD:
-  "non_empty step ==> \<exists>q t'. (q,t') \<in> set(step p t)"
+  "non_empty step \<Longrightarrow> \<exists>q t'. (q,t') \<in> set(step p t)"
 proof (unfold non_empty_def)
   assume "\<forall>p t. step p t \<noteq> []"
   hence "step p t \<noteq> []" by blast
@@ -47,9 +47,9 @@
 
 
 lemma dynamic_imp_static:
-  "[| bounded step (size ts); non_empty step;
-      dynamic_wt r (err_step app step) ts |] 
-  ==> static_wt r app step (map ok_val ts)"
+  "\<lbrakk> bounded step (size ts); non_empty step;
+      dynamic_wt r (err_step app step) ts \<rbrakk> 
+  \<Longrightarrow> static_wt r app step (map ok_val ts)"
 proof (unfold static_wt_def, intro strip, rule conjI)
 
   assume b:  "bounded step (size ts)"
@@ -112,8 +112,8 @@
 
 
 lemma static_imp_dynamic:
-  "[| static_wt r app step ts; bounded step (size ts) |] 
-  ==> dynamic_wt r (err_step app step) (map OK ts)"
+  "\<lbrakk> static_wt r app step ts; bounded step (size ts) \<rbrakk> 
+  \<Longrightarrow> dynamic_wt r (err_step app step) (map OK ts)"
 proof (unfold dynamic_wt_def wt_step_def, intro strip, rule conjI)
   assume bounded: "bounded step (size ts)"
   assume static:  "static_wt r app step ts"