diff -r 42a54d6cec15 -r 51c5f3f11d16 src/HOL/MicroJava/BV/Semilat.thy
--- a/src/HOL/MicroJava/BV/Semilat.thy	Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Sun Mar 03 16:59:08 2002 +0100
@@ -13,134 +13,134 @@
 
 theory Semilat = While_Combinator:
 
-types 'a ord    = "'a => 'a => bool"
-      'a binop  = "'a => 'a => 'a"
+types 'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
+      'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"
       'a sl     = "'a set * 'a ord * 'a binop"
 
 consts
- "@lesub"   :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
- "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
+ "@lesub"   :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
+ "@lesssub" :: "'a \<Rightarrow> 'a ord \<Rightarrow> 'a \<Rightarrow> bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
 defs
 lesub_def:   "x <=_r y == r x y"
 lesssub_def: "x <_r y  == x <=_r y & x ~= y"
 
 consts
- "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
+ "@plussub" :: "'a \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
 defs
 plussub_def: "x +_f y == f x y"
 
 
 constdefs
- ord :: "('a*'a)set => 'a ord"
+ ord :: "('a*'a)set \<Rightarrow> 'a ord"
 "ord r == %x y. (x,y):r"
 
- order :: "'a ord => bool"
+ order :: "'a ord \<Rightarrow> bool"
 "order r == (!x. x <=_r x) &
-            (!x y. x <=_r y & y <=_r x --> x=y) &
-            (!x y z. x <=_r y & y <=_r z --> x <=_r z)"
+            (!x y. x <=_r y & y <=_r x \<longrightarrow> x=y) &
+            (!x y z. x <=_r y & y <=_r z \<longrightarrow> x <=_r z)"
 
- acc :: "'a ord => bool"
+ acc :: "'a ord \<Rightarrow> bool"
 "acc r == wf{(y,x) . x <_r y}"
 
- top :: "'a ord => 'a => bool"
+ top :: "'a ord \<Rightarrow> 'a \<Rightarrow> bool"
 "top r T == !x. x <=_r T"
 
- closed :: "'a set => 'a binop => bool"
+ closed :: "'a set \<Rightarrow> 'a binop \<Rightarrow> bool"
 "closed A f == !x:A. !y:A. x +_f y : A"
 
- semilat :: "'a sl => bool"
+ semilat :: "'a sl \<Rightarrow> bool"
 "semilat == %(A,r,f). order r & closed A f &
                 (!x:A. !y:A. x <=_r x +_f y)  &
                 (!x:A. !y:A. y <=_r x +_f y)  &
-                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
 
- is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
+ is_ub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
 "is_ub r x y u == (x,u):r & (y,u):r"
 
- is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
-"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+ is_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
 
- some_lub :: "('a*'a)set => 'a => 'a => 'a"
+ some_lub :: "('a*'a)set \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
 "some_lub r x y == SOME z. is_lub r x y z"
 
 
 lemma order_refl [simp, intro]:
-  "order r ==> x <=_r x";
+  "order r \<Longrightarrow> x <=_r x";
   by (simp add: order_def)
 
 lemma order_antisym:
-  "[| order r; x <=_r y; y <=_r x |] ==> x = y"
+  "\<lbrakk> order r; x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
 apply (unfold order_def)
 apply (simp (no_asm_simp))  
 done
 
 lemma order_trans:
-   "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"
+   "\<lbrakk> order r; x <=_r y; y <=_r z \<rbrakk> \<Longrightarrow> x <=_r z"
 apply (unfold order_def)
 apply blast
 done 
 
 lemma order_less_irrefl [intro, simp]:
-   "order r ==> ~ x <_r x"
+   "order r \<Longrightarrow> ~ x <_r x"
 apply (unfold order_def lesssub_def)
 apply blast
 done 
 
 lemma order_less_trans:
-  "[| order r; x <_r y; y <_r z |] ==> x <_r z"
+  "\<lbrakk> order r; x <_r y; y <_r z \<rbrakk> \<Longrightarrow> x <_r z"
 apply (unfold order_def lesssub_def)
 apply blast
 done 
 
 lemma topD [simp, intro]:
-  "top r T ==> x <=_r T"
+  "top r T \<Longrightarrow> x <=_r T"
   by (simp add: top_def)
 
 lemma top_le_conv [simp]:
-  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
+  "\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
   by (blast intro: order_antisym)
 
 lemma semilat_Def:
 "semilat(A,r,f) == order r & closed A f & 
                  (!x:A. !y:A. x <=_r x +_f y) & 
                  (!x:A. !y:A. y <=_r x +_f y) & 
-                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z \<longrightarrow> x +_f y <=_r z)"
 apply (unfold semilat_def split_conv [THEN eq_reflection])
 apply (rule refl [THEN eq_reflection])
 done
 
 lemma semilatDorderI [simp, intro]:
-  "semilat(A,r,f) ==> order r"
+  "semilat(A,r,f) \<Longrightarrow> order r"
   by (simp add: semilat_Def)
 
 lemma semilatDclosedI [simp, intro]:
-  "semilat(A,r,f) ==> closed A f"
+  "semilat(A,r,f) \<Longrightarrow> closed A f"
 apply (unfold semilat_Def)
 apply simp
 done
 
 lemma semilat_ub1 [simp]:
-  "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"
+  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
   by (unfold semilat_Def, simp)
 
 lemma semilat_ub2 [simp]:
-  "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"
+  "\<lbrakk> semilat(A,r,f); x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
   by (unfold semilat_Def, simp)
 
 lemma semilat_lub [simp]:
- "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
+ "\<lbrakk> x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
   by (unfold semilat_Def, simp)
 
 
 lemma plus_le_conv [simp]:
-  "[| x:A; y:A; z:A; semilat(A,r,f) |] 
-  ==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
+  "\<lbrakk> x:A; y:A; z:A; semilat(A,r,f) \<rbrakk> 
+  \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
 apply (unfold semilat_Def)
 apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
 done
 
 lemma le_iff_plus_unchanged:
-  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)"
+  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
 apply (rule iffI)
  apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
 apply (erule subst)
@@ -148,7 +148,7 @@
 done 
 
 lemma le_iff_plus_unchanged2:
-  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)"
+  "\<lbrakk> x:A; y:A; semilat(A,r,f) \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
 apply (rule iffI)
  apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
 apply (erule subst)
@@ -157,7 +157,7 @@
 
 
 lemma closedD:
-  "[| closed A f; x:A; y:A |] ==> x +_f y : A"
+  "\<lbrakk> closed A f; x:A; y:A \<rbrakk> \<Longrightarrow> x +_f y : A"
 apply (unfold closed_def)
 apply blast
 done 
@@ -167,15 +167,15 @@
 
 
 lemma is_lubD:
-  "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+  "is_lub r x y u \<Longrightarrow> is_ub r x y u & (!z. is_ub r x y z \<longrightarrow> (u,z):r)"
   by (simp add: is_lub_def)
 
 lemma is_ubI:
-  "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"
+  "\<lbrakk> (x,u) : r; (y,u) : r \<rbrakk> \<Longrightarrow> is_ub r x y u"
   by (simp add: is_ub_def)
 
 lemma is_ubD:
-  "is_ub r x y u ==> (x,u) : r & (y,u) : r"
+  "is_ub r x y u \<Longrightarrow> (x,u) : r & (y,u) : r"
   by (simp add: is_ub_def)
 
 
@@ -192,8 +192,8 @@
 done
 
 lemma extend_lub:
-  "[| single_valued r; is_lub (r^* ) x y u; (x',x) : r |] 
-  ==> EX v. is_lub (r^* ) x' y v"
+  "\<lbrakk> single_valued r; is_lub (r^* ) x y u; (x',x) : r \<rbrakk> 
+  \<Longrightarrow> EX v. is_lub (r^* ) x' y v"
 apply (unfold is_lub_def is_ub_def)
 apply (case_tac "(y,x) : r^*")
  apply (case_tac "(y,x') : r^*")
@@ -207,7 +207,7 @@
 done
 
 lemma single_valued_has_lubs [rule_format]:
-  "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> 
+  "\<lbrakk> single_valued r; (x,u) : r^* \<rbrakk> \<Longrightarrow> (!y. (y,u) : r^* \<longrightarrow> 
   (EX z. is_lub (r^* ) x y z))"
 apply (erule converse_rtrancl_induct)
  apply clarify
@@ -218,7 +218,7 @@
 done
 
 lemma some_lub_conv:
-  "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u"
+  "\<lbrakk> acyclic r; is_lub (r^* ) x y u \<rbrakk> \<Longrightarrow> some_lub (r^* ) x y = u"
 apply (unfold some_lub_def is_lub_def)
 apply (rule someI2)
  apply assumption
@@ -226,8 +226,8 @@
 done
 
 lemma is_lub_some_lub:
-  "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] 
-  ==> is_lub (r^* ) x y (some_lub (r^* ) x y)";
+  "\<lbrakk> single_valued r; acyclic r; (x,u):r^*; (y,u):r^* \<rbrakk> 
+  \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
   by (fastsimp dest: single_valued_has_lubs simp add: some_lub_conv)
 
 subsection{*An executable lub-finder*}