diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Err.thy
--- a/src/HOL/MicroJava/BV/Err.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Err.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -12,48 +12,48 @@
 
 datatype 'a err = Err | OK 'a
 
-types 'a ebinop = "'a => 'a => 'a err"
+types 'a ebinop = "'a \<Rightarrow> 'a \<Rightarrow> 'a err"
       'a esl =    "'a set * 'a ord * 'a ebinop"
 
 consts
-  ok_val :: "'a err => 'a"
+  ok_val :: "'a err \<Rightarrow> 'a"
 primrec
   "ok_val (OK x) = x"
 
 constdefs
- lift :: "('a => 'b err) => ('a err => 'b err)"
-"lift f e == case e of Err => Err | OK x => f x"
+ lift :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+"lift f e == case e of Err \<Rightarrow> Err | OK x \<Rightarrow> f x"
 
- lift2 :: "('a => 'b => 'c err) => 'a err => 'b err => 'c err"
+ lift2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a err \<Rightarrow> 'b err \<Rightarrow> 'c err"
 "lift2 f e1 e2 ==
- case e1 of Err  => Err
-          | OK x => (case e2 of Err => Err | OK y => f x y)"
+ case e1 of Err  \<Rightarrow> Err
+          | OK x \<Rightarrow> (case e2 of Err \<Rightarrow> Err | OK y \<Rightarrow> f x y)"
 
- le :: "'a ord => 'a err ord"
+ le :: "'a ord \<Rightarrow> 'a err ord"
 "le r e1 e2 ==
-        case e2 of Err => True |
-                   OK y => (case e1 of Err => False | OK x => x <=_r y)"
+        case e2 of Err \<Rightarrow> True |
+                   OK y \<Rightarrow> (case e1 of Err \<Rightarrow> False | OK x \<Rightarrow> x <=_r y)"
 
- sup :: "('a => 'b => 'c) => ('a err => 'b err => 'c err)"
+ sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> 'c err)"
 "sup f == lift2(%x y. OK(x +_f y))"
 
- err :: "'a set => 'a err set"
+ err :: "'a set \<Rightarrow> 'a err set"
 "err A == insert Err {x . ? y:A. x = OK y}"
 
- esl :: "'a sl => 'a esl"
+ esl :: "'a sl \<Rightarrow> 'a esl"
 "esl == %(A,r,f). (A,r, %x y. OK(f x y))"
 
- sl :: "'a esl => 'a err sl"
+ sl :: "'a esl \<Rightarrow> 'a err sl"
 "sl == %(A,r,f). (err A, le r, lift2 f)"
 
 syntax
- err_semilat :: "'a esl => bool"
+ err_semilat :: "'a esl \<Rightarrow> bool"
 translations
 "err_semilat L" == "semilat(Err.sl L)"
 
 
 consts
-  strict  :: "('a => 'b err) => ('a err => 'b err)"
+  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
 primrec
   "strict f Err    = Err"
   "strict f (OK x) = f x"
@@ -75,20 +75,20 @@
   by (simp add: lesub_def)
 
 lemma le_err_refl:
-  "!x. x <=_r x ==> e <=_(Err.le r) e"
+  "!x. x <=_r x \<Longrightarrow> e <=_(Err.le r) e"
 apply (unfold lesub_def Err.le_def)
 apply (simp split: err.split)
 done 
 
 lemma le_err_trans [rule_format]:
-  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"
+  "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e3 \<longrightarrow> e1 <=_(le r) e3"
 apply (unfold unfold_lesub_err le_def)
 apply (simp split: err.split)
 apply (blast intro: order_trans)
 done
 
 lemma le_err_antisym [rule_format]:
-  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"
+  "order r \<Longrightarrow> e1 <=_(le r) e2 \<longrightarrow> e2 <=_(le r) e1 \<longrightarrow> e1=e2"
 apply (unfold unfold_lesub_err le_def)
 apply (simp split: err.split)
 apply (blast intro: order_antisym)
@@ -136,20 +136,20 @@
   by (simp add: lesssub_def lesub_def le_def split: err.split)
 
 lemma semilat_errI:
-  "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+  "semilat(A,r,f) \<Longrightarrow> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
 apply (unfold semilat_Def closed_def plussub_def lesub_def 
               lift2_def Err.le_def err_def)
 apply (simp split: err.split)
 done
 
 lemma err_semilat_eslI: 
-  "!!L. semilat L ==> err_semilat(esl L)"
+  "\<And>L. semilat L \<Longrightarrow> err_semilat(esl L)"
 apply (unfold sl_def esl_def)
 apply (simp (no_asm_simp) only: split_tupled_all)
 apply (simp add: semilat_errI)
 done
 
-lemma acc_err [simp, intro!]:  "acc r ==> acc(le r)"
+lemma acc_err [simp, intro!]:  "acc r \<Longrightarrow> acc(le r)"
 apply (unfold acc_def lesub_def le_def lesssub_def)
 apply (simp add: wf_eq_minimal split: err.split)
 apply clarify
@@ -170,7 +170,7 @@
 section {* lift *}
 
 lemma lift_in_errI:
-  "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
+  "\<lbrakk> e : err S; !x:S. e = OK x \<longrightarrow> f x : err S \<rbrakk> \<Longrightarrow> lift f e : err S"
 apply (unfold lift_def)
 apply (simp split: err.split)
 apply blast
@@ -221,42 +221,42 @@
 section {* semilat (err A) (le r) f *}
 
 lemma semilat_le_err_Err_plus [simp]:
-  "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
+  "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
   by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
 
 lemma semilat_le_err_plus_Err [simp]:
-  "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"
+  "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
   by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
 
 lemma semilat_le_err_OK1:
-  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
-  ==> x <=_r z";
+  "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
+  \<Longrightarrow> x <=_r z";
 apply (rule OK_le_err_OK [THEN iffD1])
 apply (erule subst)
 apply simp
 done 
 
 lemma semilat_le_err_OK2:
-  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
-  ==> y <=_r z"
+  "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
+  \<Longrightarrow> y <=_r z"
 apply (rule OK_le_err_OK [THEN iffD1])
 apply (erule subst)
 apply simp
 done 
 
 lemma eq_order_le:
-  "[| x=y; order r |] ==> x <=_r y"
+  "\<lbrakk> x=y; order r \<rbrakk> \<Longrightarrow> x <=_r y"
 apply (unfold order_def)
 apply blast
 done
 
 lemma OK_plus_OK_eq_Err_conv [simp]:
-  "[| x:A; y:A; semilat(err A, le r, fe) |] ==> 
+  "\<lbrakk> x:A; y:A; semilat(err A, le r, fe) \<rbrakk> \<Longrightarrow> 
   ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
 proof -
-  have plus_le_conv3: "!!A x y z f r. 
-    [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
-    ==> x <=_r z \<and> y <=_r z"
+  have plus_le_conv3: "\<And>A x y z f r. 
+    \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> 
+    \<Longrightarrow> x <=_r z \<and> y <=_r z"
     by (rule plus_le_conv [THEN iffD1])
   case rule_context
   thus ?thesis
@@ -287,13 +287,13 @@
 
 (* FIXME? *)
 lemma all_bex_swap_lemma [iff]:
-  "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"
+  "(!x. (? y:A. x = f y) \<longrightarrow> P x) = (!y:A. P(f y))"
   by blast
 
 lemma closed_err_Union_lift2I: 
-  "[| !A:AS. closed (err A) (lift2 f); AS ~= {}; 
-      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] 
-  ==> closed (err(Union AS)) (lift2 f)"
+  "\<lbrakk> !A:AS. closed (err A) (lift2 f); AS ~= {}; 
+      !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. a +_f b = Err) \<rbrakk> 
+  \<Longrightarrow> closed (err(Union AS)) (lift2 f)"
 apply (unfold closed_def err_def)
 apply simp
 apply clarify
@@ -307,9 +307,9 @@
   which may not hold 
 *}
 lemma err_semilat_UnionI:
-  "[| !A:AS. err_semilat(A, r, f); AS ~= {}; 
-      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] 
-  ==> err_semilat(Union AS, r, f)"
+  "\<lbrakk> !A:AS. err_semilat(A, r, f); AS ~= {}; 
+      !A:AS.!B:AS. A~=B \<longrightarrow> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) \<rbrakk> 
+  \<Longrightarrow> err_semilat(Union AS, r, f)"
 apply (unfold semilat_def sl_def)
 apply (simp add: closed_err_Union_lift2I)
 apply (rule conjI)