# HG changeset patch
# User paulson
# Date 1331052387 0
# Node ID 95f1e700b712d2ef96bfca7fd71e67a1864f17a5
# Parent  ff6b0c1087f27dc8b7dcda7384a3439e65dd456c
 mathematical symbols for Isabelle/ZF example theories

diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC15_WO6.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -42,11 +42,11 @@
      "0\<notin>A ==> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. ~Finite(B)"
 apply clarify 
 apply (rule nat_not_Finite [THEN notE] )
-apply (subgoal_tac "x ~= 0")
+apply (subgoal_tac "x \<noteq> 0")
  apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
 done
 
-lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
+lemma lemma1: "[| \<Union>(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
 by fast
 
 lemma lemma2: 
@@ -55,7 +55,7 @@
 
 lemma lemma3: 
      "\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) &   
-             sets_of_size_between(f`B, 2, n) & Union(f`B)=B   
+             sets_of_size_between(f`B, 2, n) & \<Union>(f`B)=B   
      ==> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) & u \<subseteq> cons(0, B*nat) &   
              0 \<in> u & 2 \<lesssim> u & u \<lesssim> n"
 apply (unfold sets_of_size_between_def)
@@ -104,7 +104,7 @@
 lemma ex_fun_AC13_AC15:
      "[| \<forall>B \<in> {cons(0, x*nat). x \<in> A}.   
                 pairwise_disjoint(f`B) &   
-                sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B; 
+                sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B; 
          n \<in> nat |]   
       ==> \<exists>f. \<forall>B \<in> A. f`B \<noteq> 0 & f`B \<subseteq> B & f`B \<lesssim> n"
 by (fast del: subsetI notI
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC16_WO4.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -47,8 +47,8 @@
 
 lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll];
 
-lemma lemma2: "\<exists>y R. well_ord(y,R) & x Int y = 0 & ~y \<lesssim> z & ~Finite(y)"
-apply (rule_tac x = "{{a,x}. a \<in> nat Un Hartog (z) }" in exI)
+lemma lemma2: "\<exists>y R. well_ord(y,R) & x \<inter> y = 0 & ~y \<lesssim> z & ~Finite(y)"
+apply (rule_tac x = "{{a,x}. a \<in> nat \<union> Hartog (z) }" in exI)
 apply (rule well_ord_Un [OF Ord_nat [THEN well_ord_Memrel] 
                          Ord_Hartog [THEN well_ord_Memrel], THEN exE])
 apply (blast intro!: Ord_Hartog well_ord_Memrel well_ord_paired
@@ -60,11 +60,11 @@
               lepoll_paired [THEN lepoll_Finite])
 done
 
-lemma infinite_Un: "~Finite(B) ==> ~Finite(A Un B)"
+lemma infinite_Un: "~Finite(B) ==> ~Finite(A \<union> B)"
 by (blast intro: subset_Finite)
 
 (* ********************************************************************** *)
-(* There is a v \<in> s(u) such that k \<lesssim> x Int y (in our case succ(k))    *)
+(* There is a v \<in> s(u) such that k \<lesssim> x \<inter> y (in our case succ(k))    *)
 (* The idea of the proof is the following \<in>                               *)
 (* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y   *)
 (* Thence y is less than or equipollent to {v \<in> Pow(x). v \<approx> n#-k}      *)
@@ -100,11 +100,11 @@
        ordermap_bij [THEN exI [THEN eqpoll_def [THEN def_imp_iff, THEN iffD2]]]
 
 lemma cons_cons_subset:
-     "[| a \<subseteq> y; b \<in> y-a; u \<in> x |] ==> cons(b, cons(u, a)) \<in> Pow(x Un y)"
+     "[| a \<subseteq> y; b \<in> y-a; u \<in> x |] ==> cons(b, cons(u, a)) \<in> Pow(x \<union> y)"
 by fast
 
 lemma cons_cons_eqpoll:
-     "[| a \<approx> k; a \<subseteq> y; b \<in> y-a; u \<in> x; x Int y = 0 |]    
+     "[| a \<approx> k; a \<subseteq> y; b \<in> y-a; u \<in> x; x \<inter> y = 0 |]    
       ==> cons(b, cons(u, a)) \<approx> succ(succ(k))"
 by (fast intro!: cons_eqpoll_succ)
 
@@ -124,7 +124,7 @@
 lemma cons_eqE: "[| cons(x,a) = cons(y,a); x \<notin> a |] ==> x = y "
 by (fast elim!: equalityE)
 
-lemma eq_imp_Int_eq: "A = B ==> A Int C = B Int C"
+lemma eq_imp_Int_eq: "A = B ==> A \<inter> C = B \<inter> C"
 by blast
 
 (* ********************************************************************** *)
@@ -133,7 +133,7 @@
 
 lemma eqpoll_sum_imp_Diff_lepoll_lemma [rule_format]:
      "[| k \<in> nat; m \<in> nat |] 
-      ==> \<forall>A B. A \<approx> k #+ m & k \<lesssim> B & B \<subseteq> A --> A-B \<lesssim> m"
+      ==> \<forall>A B. A \<approx> k #+ m & k \<lesssim> B & B \<subseteq> A \<longrightarrow> A-B \<lesssim> m"
 apply (induct_tac "k")
 apply (simp add: add_0)
 apply (blast intro: eqpoll_imp_lepoll lepoll_trans
@@ -162,7 +162,7 @@
 
 lemma eqpoll_sum_imp_Diff_eqpoll_lemma [rule_format]:
      "[| k \<in> nat; m \<in> nat |] 
-      ==> \<forall>A B. A \<approx> k #+ m & k \<approx> B & B \<subseteq> A --> A-B \<approx> m"
+      ==> \<forall>A B. A \<approx> k #+ m & k \<approx> B & B \<subseteq> A \<longrightarrow> A-B \<approx> m"
 apply (induct_tac "k")
 apply (force dest!: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_0_is_0])
 apply (intro allI impI)
@@ -193,27 +193,27 @@
 
 lemma subsets_lepoll_succ:
      "n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> succ(n)} =   
-                  {z \<in> Pow(y). z \<lesssim> n} Un {z \<in> Pow(y). z \<approx> succ(n)}"
+                  {z \<in> Pow(y). z \<lesssim> n} \<union> {z \<in> Pow(y). z \<approx> succ(n)}"
 by (blast intro: leI le_imp_lepoll nat_into_Ord 
                     lepoll_trans eqpoll_imp_lepoll
           dest!: lepoll_succ_disj)
 
 lemma Int_empty:
-     "n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> n} Int {z \<in> Pow(y). z \<approx> succ(n)} = 0"
+     "n \<in> nat ==> {z \<in> Pow(y). z \<lesssim> n} \<inter> {z \<in> Pow(y). z \<approx> succ(n)} = 0"
 by (blast intro: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
                  succ_lepoll_natE)
 
 locale AC16 =
   fixes x and y and k and l and m and t_n and R and MM and LL and GG and s 
   defines k_def:     "k   == succ(l)"
-      and MM_def:    "MM  == {v \<in> t_n. succ(k) \<lesssim> v Int y}"
-      and LL_def:    "LL  == {v Int y. v \<in> MM}"
+      and MM_def:    "MM  == {v \<in> t_n. succ(k) \<lesssim> v \<inter> y}"
+      and LL_def:    "LL  == {v \<inter> y. v \<in> MM}"
       and GG_def:    "GG  == \<lambda>v \<in> LL. (THE w. w \<in> MM & v \<subseteq> w) - v"
-      and s_def:     "s(u) == {v \<in> t_n. u \<in> v & k \<lesssim> v Int y}"
-  assumes all_ex:    "\<forall>z \<in> {z \<in> Pow(x Un y) . z \<approx> succ(k)}.
+      and s_def:     "s(u) == {v \<in> t_n. u \<in> v & k \<lesssim> v \<inter> y}"
+  assumes all_ex:    "\<forall>z \<in> {z \<in> Pow(x \<union> y) . z \<approx> succ(k)}.
                        \<exists>! w. w \<in> t_n & z \<subseteq> w "
-    and disjoint[iff]:  "x Int y = 0"
-    and "includes":  "t_n \<subseteq> {v \<in> Pow(x Un y). v \<approx> succ(k #+ m)}"
+    and disjoint[iff]:  "x \<inter> y = 0"
+    and "includes":  "t_n \<subseteq> {v \<in> Pow(x \<union> y). v \<approx> succ(k #+ m)}"
     and WO_R[iff]:      "well_ord(y,R)"
     and lnat[iff]:      "l \<in> nat"
     and mnat[iff]:      "m \<in> nat"
@@ -274,16 +274,16 @@
 done
 
 lemma (in AC16) the_eq_cons:
-     "[| \<forall>v \<in> s(u). succ(l) \<approx> v Int y;   
+     "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;   
          l \<approx> a;  a \<subseteq> y;  b \<in> y - a;  u \<in> x |]    
-      ==> (THE c. c \<in> s(u) & a \<subseteq> c & b \<in> c) Int y = cons(b, a)"
+      ==> (THE c. c \<in> s(u) & a \<subseteq> c & b \<in> c) \<inter> y = cons(b, a)"
 apply (frule ex1_superset_a [THEN theI], assumption+)
 apply (rule set_eq_cons)
 apply (fast+)
 done
 
 lemma (in AC16) y_lepoll_subset_s:
-     "[| \<forall>v \<in> s(u). succ(l) \<approx> v Int y;   
+     "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y;   
          l \<approx> a;  a \<subseteq> y;  u \<in> x |]   
       ==> y \<lesssim> {v \<in> s(u). a \<subseteq> v}"
 apply (rule Diff_Finite_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, 
@@ -310,14 +310,14 @@
 by (blast dest:  disjoint [THEN equalityD1, THEN subsetD, OF IntI])
 
 lemma (in AC16) w_Int_eq_w_Diff:
-     "w \<subseteq> x Un y ==> w Int (x - {u}) = w - cons(u, w Int y)" 
+     "w \<subseteq> x \<union> y ==> w \<inter> (x - {u}) = w - cons(u, w \<inter> y)" 
 by blast
 
 lemma (in AC16) w_Int_eqpoll_m:
      "[| w \<in> {v \<in> s(u). a \<subseteq> v};   
          l \<approx> a;  u \<in> x;   
-         \<forall>v \<in> s(u). succ(l) \<approx> v Int y |] 
-      ==> w Int (x - {u}) \<approx> m"
+         \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y |] 
+      ==> w \<inter> (x - {u}) \<approx> m"
 apply (erule CollectE)
 apply (subst w_Int_eq_w_Diff)
 apply (fast dest!: s_subset [THEN subsetD] 
@@ -341,7 +341,7 @@
 done
 
 lemma (in AC16) cons_cons_in:
-     "[| z \<in> xa Int (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x |]   
+     "[| z \<in> xa \<inter> (x - {u}); l \<approx> a; a \<subseteq> y; u \<in> x |]   
       ==> \<exists>! w. w \<in> t_n & cons(z, cons(u, a)) \<subseteq> w"
 apply (rule all_ex [THEN bspec])
 apply (unfold k_def)
@@ -349,9 +349,9 @@
 done
 
 lemma (in AC16) subset_s_lepoll_w:
-     "[| \<forall>v \<in> s(u). succ(l) \<approx> v Int y; a \<subseteq> y; l \<approx> a; u \<in> x |]   
+     "[| \<forall>v \<in> s(u). succ(l) \<approx> v \<inter> y; a \<subseteq> y; l \<approx> a; u \<in> x |]   
       ==> {v \<in> s(u). a \<subseteq> v} \<lesssim> {v \<in> Pow(x). v \<approx> m}"
-apply (rule_tac f3 = "\<lambda>w \<in> {v \<in> s (u) . a \<subseteq> v}. w Int (x - {u})" 
+apply (rule_tac f3 = "\<lambda>w \<in> {v \<in> s (u) . a \<subseteq> v}. w \<inter> (x - {u})" 
        in exI [THEN lepoll_def [THEN def_imp_iff, THEN iffD2]])
 apply (simp add: inj_def)
 apply (intro conjI lam_type CollectI)
@@ -425,11 +425,11 @@
 (* The union of appropriate values is the whole x                         *)
 (* ********************************************************************** *)
 
-lemma (in AC16) Int_in_LL: "w \<in> MM ==> w Int y \<in> LL"
+lemma (in AC16) Int_in_LL: "w \<in> MM ==> w \<inter> y \<in> LL"
 by (unfold LL_def, fast)
 
 lemma (in AC16) in_LL_eq_Int: 
-     "v \<in> LL ==> v = (THE x. x \<in> MM & v \<subseteq> x) Int y"
+     "v \<in> LL ==> v = (THE x. x \<in> MM & v \<subseteq> x) \<inter> y"
 apply (unfold LL_def, clarify)
 apply (subst unique_superset_in_MM [THEN the_equality2])
 apply (auto simp add: Int_in_LL)
@@ -439,7 +439,7 @@
 by (erule unique_superset_in_MM [THEN theI, THEN conjunct1]) 
 
 lemma (in AC16) the_in_MM_subset:
-     "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x Un y"
+     "v \<in> LL ==> (THE x. x \<in> MM & v \<subseteq> x) \<subseteq> x \<union> y"
 apply (drule unique_superset1)
 apply (unfold MM_def)
 apply (fast dest!: unique_superset1 "includes" [THEN subsetD])
@@ -468,9 +468,9 @@
 done
 
 
-lemma (in AC16) exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v Int y"
+lemma (in AC16) exists_proper_in_s: "u \<in> x ==> \<exists>v \<in> s(u). succ(k) \<lesssim> v \<inter> y"
 apply (rule ccontr)
-apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v Int y")
+apply (subgoal_tac "\<forall>v \<in> s (u) . k \<approx> v \<inter> y")
 prefer 2 apply (simp add: s_def, blast intro: succ_not_lepoll_imp_eqpoll)
 apply (unfold k_def)
 apply (insert all_ex "includes" lnat)
@@ -568,7 +568,7 @@
 apply (rule lemma1, assumption+)
 apply (cut_tac lemma2)
 apply (elim exE conjE)
-apply (erule_tac x = "A Un y" in allE)
+apply (erule_tac x = "A \<union> y" in allE)
 apply (frule infinite_Un, drule mp, assumption)
 apply (erule zero_lt_natE, assumption, clarify)
 apply (blast intro: AC16.conclusion [OF AC16.intro])
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC16_lemmas.thy
--- a/src/ZF/AC/AC16_lemmas.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC16_lemmas.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -11,7 +11,7 @@
 lemma cons_Diff_eq: "a\<notin>A ==> cons(a,A)-{a}=A"
 by fast
 
-lemma nat_1_lepoll_iff: "1\<lesssim>X <-> (\<exists>x. x \<in> X)"
+lemma nat_1_lepoll_iff: "1\<lesssim>X \<longleftrightarrow> (\<exists>x. x \<in> X)"
 apply (unfold lepoll_def)
 apply (rule iffI)
 apply (fast intro: inj_is_fun [THEN apply_type])
@@ -20,7 +20,7 @@
 apply (fast intro!: lam_injective)
 done
 
-lemma eqpoll_1_iff_singleton: "X\<approx>1 <-> (\<exists>x. X={x})"
+lemma eqpoll_1_iff_singleton: "X\<approx>1 \<longleftrightarrow> (\<exists>x. X={x})"
 apply (rule iffI)
 apply (erule eqpollE)
 apply (drule nat_1_lepoll_iff [THEN iffD1])
@@ -79,7 +79,7 @@
 apply (simp, blast intro: InfCard_Least_in)
 done
 
-lemma set_of_Ord_succ_Union: "(\<forall>y \<in> z. Ord(y)) ==> z \<subseteq> succ(Union(z))"
+lemma set_of_Ord_succ_Union: "(\<forall>y \<in> z. Ord(y)) ==> z \<subseteq> succ(\<Union>(z))"
 apply (rule subsetI)
 apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast )
 apply (simp, erule bexE) 
@@ -91,22 +91,22 @@
 by (fast elim!: mem_irrefl)
 
 lemma succ_Union_not_mem:
-     "(!!y. y \<in> z ==> Ord(y)) ==> succ(Union(z)) \<notin> z"
+     "(!!y. y \<in> z ==> Ord(y)) ==> succ(\<Union>(z)) \<notin> z"
 apply (rule set_of_Ord_succ_Union [THEN subset_not_mem], blast)
 done
 
 lemma Union_cons_eq_succ_Union:
-     "Union(cons(succ(Union(z)),z)) = succ(Union(z))"
+     "\<Union>(cons(succ(\<Union>(z)),z)) = succ(\<Union>(z))"
 by fast
 
-lemma Un_Ord_disj: "[| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j"
+lemma Un_Ord_disj: "[| Ord(i); Ord(j) |] ==> i \<union> j = i | i \<union> j = j"
 by (fast dest!: le_imp_subset elim: Ord_linear_le)
 
-lemma Union_eq_Un: "x \<in> X ==> Union(X) = x Un Union(X-{x})"
+lemma Union_eq_Un: "x \<in> X ==> \<Union>(X) = x \<union> \<Union>(X-{x})"
 by fast
 
 lemma Union_in_lemma [rule_format]:
-     "n \<in> nat ==> \<forall>z. (\<forall>y \<in> z. Ord(y)) & z\<approx>n & z\<noteq>0 --> Union(z) \<in> z"
+     "n \<in> nat ==> \<forall>z. (\<forall>y \<in> z. Ord(y)) & z\<approx>n & z\<noteq>0 \<longrightarrow> \<Union>(z) \<in> z"
 apply (induct_tac "n")
 apply (fast dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
 apply (intro allI impI)
@@ -126,11 +126,11 @@
 apply (drule Un_Ord_disj, assumption, auto) 
 done
 
-lemma Union_in: "[| \<forall>x \<in> z. Ord(x); z\<approx>n; z\<noteq>0; n \<in> nat |] ==> Union(z) \<in> z"
+lemma Union_in: "[| \<forall>x \<in> z. Ord(x); z\<approx>n; z\<noteq>0; n \<in> nat |] ==> \<Union>(z) \<in> z"
 by (blast intro: Union_in_lemma)
 
 lemma succ_Union_in_x:
-     "[| InfCard(x); z \<in> Pow(x); z\<approx>n; n \<in> nat |] ==> succ(Union(z)) \<in> x"
+     "[| InfCard(x); z \<in> Pow(x); z\<approx>n; n \<in> nat |] ==> succ(\<Union>(z)) \<in> x"
 apply (rule Limit_has_succ [THEN ltE])
 prefer 3 apply assumption
 apply (erule InfCard_is_Limit)
@@ -145,9 +145,9 @@
      "[| InfCard(x); n \<in> nat |] 
       ==> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
 apply (unfold lepoll_def)
-apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(Union(z)), z)" 
+apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(\<Union>(z)), z)" 
        in exI)
-apply (rule_tac d = "%z. z-{Union (z) }" in lam_injective)
+apply (rule_tac d = "%z. z-{\<Union>(z) }" in lam_injective)
 apply (blast intro!: succ_Union_in_x succ_Union_not_mem
              intro: cons_eqpoll_succ Ord_in_Ord
              dest!: InfCard_is_Card [THEN Card_is_Ord])
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC17_AC1.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -75,7 +75,7 @@
 apply (erule swap)
 apply (rule allI)
 apply (erule swap)
-apply (rule_tac x = "Union (A)" in exI)
+apply (rule_tac x = "\<Union>(A)" in exI)
 apply (blast intro: lam_type)
 done
 
@@ -136,7 +136,7 @@
     AC1 ==> AC2 ==> AC1
     AC1 ==> AC4 ==> AC3 ==> AC1
     AC4 ==> AC5 ==> AC4
-    AC1 <-> AC6
+    AC1 \<longleftrightarrow> AC6
 ************************************************************************* *)
 
 (* ********************************************************************** *)
@@ -144,7 +144,7 @@
 (* ********************************************************************** *)
 
 lemma AC1_AC2_aux1:
-     "[| f:(\<Pi> X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B Int {f`C. C \<in> A}"
+     "[| f:(\<Pi> X \<in> A. X);  B \<in> A;  0\<notin>A |] ==> {f`B} \<subseteq> B \<inter> {f`C. C \<in> A}"
 by (fast elim!: apply_type)
 
 lemma AC1_AC2_aux2: 
@@ -169,16 +169,16 @@
 lemma AC2_AC1_aux1: "0\<notin>A ==> 0 \<notin> {B*{B}. B \<in> A}"
 by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]])
 
-lemma AC2_AC1_aux2: "[| X*{X} Int C = {y}; X \<in> A |]   
-               ==> (THE y. X*{X} Int C = {y}): X*A"
+lemma AC2_AC1_aux2: "[| X*{X} \<inter> C = {y}; X \<in> A |]   
+               ==> (THE y. X*{X} \<inter> C = {y}): X*A"
 apply (rule subst_elem [of y])
 apply (blast elim!: equalityE)
 apply (auto simp add: singleton_eq_iff) 
 done
 
 lemma AC2_AC1_aux3:
-     "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D Int C = {y}   
-      ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} Int C = {z}))) \<in> (\<Pi> X \<in> A. X)"
+     "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D \<inter> C = {y}   
+      ==> (\<lambda>x \<in> A. fst(THE z. (x*{x} \<inter> C = {z}))) \<in> (\<Pi> X \<in> A. X)"
 apply (rule lam_type)
 apply (drule bspec, blast)
 apply (blast intro: AC2_AC1_aux2 fst_type)
@@ -212,7 +212,7 @@
 (* AC4 ==> AC3                                                            *)
 (* ********************************************************************** *)
 
-lemma AC4_AC3_aux1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*Union(B)"
+lemma AC4_AC3_aux1: "f \<in> A->B ==> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*\<Union>(B)"
 by (fast dest!: apply_type)
 
 lemma AC4_AC3_aux2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
@@ -292,10 +292,10 @@
 
 
 (* ********************************************************************** *)
-(* AC1 <-> AC6                                                            *)
+(* AC1 \<longleftrightarrow> AC6                                                            *)
 (* ********************************************************************** *)
 
-lemma AC1_iff_AC6: "AC1 <-> AC6"
+lemma AC1_iff_AC6: "AC1 \<longleftrightarrow> AC6"
 by (unfold AC1_def AC6_def, blast)
 
 end
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC18_AC19.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -10,7 +10,7 @@
 
 definition
   uu    :: "i => i" where
-    "uu(a) == {c Un {0}. c \<in> a}"
+    "uu(a) == {c \<union> {0}. c \<in> a}"
 
 
 (* ********************************************************************** *)
@@ -23,7 +23,7 @@
 by (rule lam_type, drule apply_type, auto)
 
 lemma lemma_AC18:
-     "[| \<forall>A. 0 \<notin> A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |] 
+     "[| \<forall>A. 0 \<notin> A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X)); A \<noteq> 0 |] 
       ==> (\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a, b)) \<subseteq> 
           (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a))"
 apply (rule subsetI)
@@ -61,7 +61,7 @@
 apply (blast dest!: sym [THEN RepFun_eq_0_iff [THEN iffD1]])
 done
 
-lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a"
+lemma lemma1_1: "[|c \<in> a; x = c \<union> {0}; x \<notin> a |] ==> x - {0} \<in> a"
 apply clarify 
 apply (rule subst_elem, assumption)
 apply (fast elim: notE subst_elem)
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC7_AC9.thy
--- a/src/ZF/AC/AC7_AC9.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC7_AC9.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -15,13 +15,13 @@
 (*  - Sigma_fun_space_eqpoll                                              *)
 (* ********************************************************************** *)
 
-lemma Sigma_fun_space_not0: "[| 0\<notin>A; B \<in> A |] ==> (nat->Union(A)) * B \<noteq> 0"
+lemma Sigma_fun_space_not0: "[| 0\<notin>A; B \<in> A |] ==> (nat->\<Union>(A)) * B \<noteq> 0"
 by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1])
 
 lemma inj_lemma: 
-        "C \<in> A ==> (\<lambda>g \<in> (nat->Union(A))*C.   
+        "C \<in> A ==> (\<lambda>g \<in> (nat->\<Union>(A))*C.   
                 (\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1))))   
-                \<in> inj((nat->Union(A))*C, (nat->Union(A)) ) "
+                \<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
 apply (unfold inj_def)
 apply (rule CollectI)
 apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) 
@@ -31,7 +31,7 @@
 done
 
 lemma Sigma_fun_space_eqpoll:
-     "[| C \<in> A; 0\<notin>A |] ==> (nat->Union(A)) * C \<approx> (nat->Union(A))"
+     "[| C \<in> A; 0\<notin>A |] ==> (nat->\<Union>(A)) * C \<approx> (nat->\<Union>(A))"
 apply (rule eqpollI)
 apply (simp add: lepoll_def)
 apply (fast intro!: inj_lemma)
@@ -62,10 +62,10 @@
 done
 
 lemma AC7_AC6_lemma1:
-     "(\<Pi> B \<in> {(nat->Union(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
+     "(\<Pi> B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 ==> (\<Pi> B \<in> A. B) \<noteq> 0"
 by (fast intro!: equals0I lemma1_1 lemma1_2)
 
-lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> Union(A)) * C. C \<in> A}"
+lemma AC7_AC6_lemma2: "0 \<notin> A ==> 0 \<notin> {(nat -> \<Union>(A)) * C. C \<in> A}"
 by (blast dest: Sigma_fun_space_not0)
 
 lemma AC7_AC6: "AC7 ==> AC6"
@@ -125,8 +125,8 @@
 (* AC9 ==> AC1                                                            *)
 (* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
 (* by Rubin & Rubin. But (x * y) is not necessarily equipollent to        *)
-(* (x * y) Un {0} when y is a set of total functions acting from nat to   *)
-(* Union(A) -- therefore we have used the set (y * nat) instead of y.     *)
+(* (x * y) \<union> {0} when y is a set of total functions acting from nat to   *)
+(* \<Union>(A) -- therefore we have used the set (y * nat) instead of y.     *)
 (* ********************************************************************** *)
 
 lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X"
@@ -134,13 +134,13 @@
                  prod_commute_eqpoll) 
 
 lemma nat_lepoll_lemma:
-     "[|0 \<notin> A; B \<in> A|] ==> nat \<lesssim> ((nat \<rightarrow> Union(A)) \<times> B) \<times> nat"
+     "[|0 \<notin> A; B \<in> A|] ==> nat \<lesssim> ((nat \<rightarrow> \<Union>(A)) \<times> B) \<times> nat"
 by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI)
 
 lemma AC9_AC1_lemma1:
      "[| 0\<notin>A;  A\<noteq>0;   
-         C = {((nat->Union(A))*B)*nat. B \<in> A}  Un  
-             {cons(0,((nat->Union(A))*B)*nat). B \<in> A};  
+         C = {((nat->\<Union>(A))*B)*nat. B \<in> A}  \<union>  
+             {cons(0,((nat->\<Union>(A))*B)*nat). B \<in> A};  
          B1 \<in> C;  B2 \<in> C |]   
       ==> B1 \<approx> B2"
 by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll
@@ -149,8 +149,8 @@
              intro: eqpoll_trans eqpoll_sym )
 
 lemma AC9_AC1_lemma2:
-     "\<forall>B1 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.   
-      \<forall>B2 \<in> {(F*B)*N. B \<in> A} Un {cons(0,(F*B)*N). B \<in> A}.   
+     "\<forall>B1 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
+      \<forall>B2 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
         f`<B1,B2> \<in> bij(B1, B2)   
       ==> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Pi> X \<in> A. X)"
 apply (intro lam_type snd_type fst_type)
@@ -162,7 +162,7 @@
 apply (unfold AC1_def AC9_def)
 apply (intro allI impI)
 apply (erule allE)
-apply (case_tac "A~=0")
+apply (case_tac "A\<noteq>0")
 apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force) 
 done
 
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/AC_Equiv.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -38,16 +38,16 @@
                                & (\<Union>b<a. f`b) = A & (\<forall>b<a. f`b \<lesssim> m))"
 
 definition  
-    "WO7 == \<forall>A. Finite(A) <-> (\<forall>R. well_ord(A,R) --> well_ord(A,converse(R)))"
+    "WO7 == \<forall>A. Finite(A) \<longleftrightarrow> (\<forall>R. well_ord(A,R) \<longrightarrow> well_ord(A,converse(R)))"
 
 definition  
-    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) --> (\<exists>R. well_ord(A,R))"
+    "WO8 == \<forall>A. (\<exists>f. f \<in> (\<Pi> X \<in> A. X)) \<longrightarrow> (\<exists>R. well_ord(A,R))"
 
 
 definition
 (* Auxiliary concepts needed below *)
   pairwise_disjoint :: "i => o"  where
-    "pairwise_disjoint(A) == \<forall>A1 \<in> A. \<forall>A2 \<in> A. A1 Int A2 \<noteq> 0 --> A1=A2"
+    "pairwise_disjoint(A) == \<forall>A1 \<in> A. \<forall>A2 \<in> A. A1 \<inter> A2 \<noteq> 0 \<longrightarrow> A1=A2"
 
 definition
   sets_of_size_between :: "[i, i, i] => o"  where
@@ -59,60 +59,60 @@
     "AC0 == \<forall>A. \<exists>f. f \<in> (\<Pi> X \<in> Pow(A)-{0}. X)"
 
 definition
-    "AC1 == \<forall>A. 0\<notin>A --> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
+    "AC1 == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. f \<in> (\<Pi> X \<in> A. X))"
 
 definition
     "AC2 == \<forall>A. 0\<notin>A & pairwise_disjoint(A)   
-                   --> (\<exists>C. \<forall>B \<in> A. \<exists>y. B Int C = {y})"
+                   \<longrightarrow> (\<exists>C. \<forall>B \<in> A. \<exists>y. B \<inter> C = {y})"
 definition
     "AC3 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g. g \<in> (\<Pi> x \<in> {a \<in> A. f`a\<noteq>0}. f`x)"
 
 definition
-    "AC4 == \<forall>R A B. (R \<subseteq> A*B --> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
+    "AC4 == \<forall>R A B. (R \<subseteq> A*B \<longrightarrow> (\<exists>f. f \<in> (\<Pi> x \<in> domain(R). R``{x})))"
 
 definition
     "AC5 == \<forall>A B. \<forall>f \<in> A->B. \<exists>g \<in> range(f)->A. \<forall>x \<in> domain(g). f`(g`x) = x"
 
 definition
-    "AC6 == \<forall>A. 0\<notin>A --> (\<Pi> B \<in> A. B)\<noteq>0"
+    "AC6 == \<forall>A. 0\<notin>A \<longrightarrow> (\<Pi> B \<in> A. B)\<noteq>0"
 
 definition
-    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) --> (\<Pi> B \<in> A. B) \<noteq> 0"
+    "AC7 == \<forall>A. 0\<notin>A & (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow> (\<Pi> B \<in> A. B) \<noteq> 0"
 
 definition
     "AC8 == \<forall>A. (\<forall>B \<in> A. \<exists>B1 B2. B=<B1,B2> & B1\<approx>B2)   
-                   --> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))"
+                   \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B \<in> bij(fst(B),snd(B)))"
 
 definition
-    "AC9 == \<forall>A. (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) -->   
+    "AC9 == \<forall>A. (\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1\<approx>B2) \<longrightarrow>   
                    (\<exists>f. \<forall>B1 \<in> A. \<forall>B2 \<in> A. f`<B1,B2> \<in> bij(B1,B2))"
 
 definition
-    "AC10(n) ==  \<forall>A. (\<forall>B \<in> A. ~Finite(B)) -->   
+    "AC10(n) ==  \<forall>A. (\<forall>B \<in> A. ~Finite(B)) \<longrightarrow>   
                    (\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) &   
-                   sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
+                   sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B))"
 
 definition
     "AC11 == \<exists>n \<in> nat. 1\<le>n & AC10(n)"
 
 definition
-    "AC12 == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) -->
+    "AC12 == \<forall>A. (\<forall>B \<in> A. ~Finite(B)) \<longrightarrow>
                  (\<exists>n \<in> nat. 1\<le>n & (\<exists>f. \<forall>B \<in> A. (pairwise_disjoint(f`B) &   
-                      sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
+                      sets_of_size_between(f`B, 2, succ(n)) & \<Union>(f`B)=B)))"
 
 definition
-    "AC13(m) == \<forall>A. 0\<notin>A --> (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m)"
+    "AC13(m) == \<forall>A. 0\<notin>A \<longrightarrow> (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m)"
 
 definition
     "AC14 == \<exists>m \<in> nat. 1\<le>m & AC13(m)"
 
 definition
-    "AC15 == \<forall>A. 0\<notin>A --> 
+    "AC15 == \<forall>A. 0\<notin>A \<longrightarrow> 
                  (\<exists>m \<in> nat. 1\<le>m & (\<exists>f. \<forall>B \<in> A. f`B\<noteq>0 & f`B \<subseteq> B & f`B \<lesssim> m))"
 
 definition
     "AC16(n, k)  == 
-       \<forall>A. ~Finite(A) -->   
+       \<forall>A. ~Finite(A) \<longrightarrow>   
            (\<exists>T. T \<subseteq> {X \<in> Pow(A). X\<approx>succ(n)} &   
            (\<forall>X \<in> {X \<in> Pow(A). X\<approx>succ(k)}. \<exists>! Y. Y \<in> T & X \<subseteq> Y))"
 
@@ -121,13 +121,13 @@
                    \<exists>f \<in> Pow(A)-{0} -> A. f`(g`f) \<in> g`f"
 
 locale AC18 =
-  assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) -->
+  assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow>
     ((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =   
       (\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
   --"AC18 cannot be expressed within the object-logic"
 
 definition
-    "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A --> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =   
+    "AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =   
                    (\<Union>f \<in> (\<Pi> B \<in> A. B). \<Inter>a \<in> A. f`a))"
 
 
@@ -137,7 +137,7 @@
 (* ********************************************************************** *)
 
 (* lemma for ordertype_Int *)
-lemma rvimage_id: "rvimage(A,id(A),r) = r Int A*A"
+lemma rvimage_id: "rvimage(A,id(A),r) = r \<inter> A*A"
 apply (unfold rvimage_def)
 apply (rule equalityI, safe)
 apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst],
@@ -148,7 +148,7 @@
 
 (* used only in Hartog.ML *)
 lemma ordertype_Int:
-     "well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"
+     "well_ord(A,r) ==> ordertype(A, r \<inter> A*A) = ordertype(A,r)"
 apply (rule_tac P = "%a. ordertype (A,a) =ordertype (A,r) " in rvimage_id [THEN subst])
 apply (erule id_bij [THEN bij_ordertype_vimage])
 done
@@ -191,11 +191,11 @@
 (* ********************************************************************** *)
 
 lemma first_in_B:
-     "[| well_ord(Union(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
+     "[| well_ord(\<Union>(A),r); 0\<notin>A; B \<in> A |] ==> (THE b. first(b,B,r)) \<in> B"
 by (blast dest!: well_ord_imp_ex1_first
                     [THEN theI, THEN first_def [THEN def_imp_iff, THEN iffD1]])
 
-lemma ex_choice_fun: "[| well_ord(Union(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
+lemma ex_choice_fun: "[| well_ord(\<Union>(A), R); 0\<notin>A |] ==> \<exists>f. f:(\<Pi> X \<in> A. X)"
 by (fast elim!: first_in_B intro!: lam_type)
 
 lemma ex_choice_fun_Pow: "well_ord(A, R) ==> \<exists>f. f:(\<Pi> X \<in> Pow(A)-{0}. X)"
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/Cardinal_aux.thy
--- a/src/ZF/AC/Cardinal_aux.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/Cardinal_aux.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -20,13 +20,13 @@
 
 (* j=|A| *)
 lemma lepoll_imp_ex_le_eqpoll:
-     "[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j le i & A \<approx> j"
-by (blast intro!: lepoll_cardinal_le well_ord_Memrel 
+     "[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j \<le> i & A \<approx> j"
+by (blast intro!: lepoll_cardinal_le well_ord_Memrel
                   well_ord_cardinal_eqpoll [THEN eqpoll_sym]
           dest: lepoll_well_ord)
 
 (* j=|A| *)
-lemma lesspoll_imp_ex_lt_eqpoll: 
+lemma lesspoll_imp_ex_lt_eqpoll:
      "[| A \<prec> i; Ord(i) |] ==> \<exists>j. j<i & A \<approx> j"
 by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE)
 
@@ -34,41 +34,41 @@
 apply (unfold InfCard_def)
 apply (rule conjI)
 apply (rule Card_cardinal)
-apply (rule Card_nat 
+apply (rule Card_nat
             [THEN Card_def [THEN def_imp_iff, THEN iffD1, THEN ssubst]])
   -- "rewriting would loop!"
-apply (rule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption) 
+apply (rule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
 apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
 done
 
 text{*An alternative and more general proof goes like this: A and B are both
-well-ordered (because they are injected into an ordinal), either A lepoll B
-or B lepoll A.  Also both are equipollent to their cardinalities, so
-(if A and B are infinite) then A Un B lepoll |A|+|B| = max(|A|,|B|) lepoll i.
+well-ordered (because they are injected into an ordinal), either @{term"A \<lesssim> B"}
+or @{term"B \<lesssim> A"}.  Also both are equipollent to their cardinalities, so
+(if A and B are infinite) then @{term"A \<union> B \<lesssim> |A\<oplus>B| \<longleftrightarrow> max(|A|,|B|) \<lesssim> i"}.
 In fact, the correctly strengthened version of this theorem appears below.*}
 lemma Un_lepoll_Inf_Ord_weak:
      "[|A \<approx> i; B \<approx> i; \<not> Finite(i); Ord(i)|] ==> A \<union> B \<lesssim> i"
 apply (rule Un_lepoll_sum [THEN lepoll_trans])
 apply (rule lepoll_imp_sum_lepoll_prod [THEN lepoll_trans])
-apply (erule eqpoll_trans [THEN eqpoll_imp_lepoll]) 
-apply (erule eqpoll_sym) 
-apply (rule subset_imp_lepoll [THEN lepoll_trans, THEN lepoll_trans]) 
-apply (rule nat_2I [THEN OrdmemD], rule Ord_nat) 
-apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+) 
-apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 
+apply (erule eqpoll_trans [THEN eqpoll_imp_lepoll])
+apply (erule eqpoll_sym)
+apply (rule subset_imp_lepoll [THEN lepoll_trans, THEN lepoll_trans])
+apply (rule nat_2I [THEN OrdmemD], rule Ord_nat)
+apply (rule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption+)
+apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
 apply (erule prod_eqpoll_cong [THEN eqpoll_imp_lepoll, THEN lepoll_trans],
        assumption)
-apply (rule eqpoll_imp_lepoll) 
-apply (rule well_ord_Memrel [THEN well_ord_InfCard_square_eq], assumption) 
-apply (rule Inf_Ord_imp_InfCard_cardinal, assumption+) 
+apply (rule eqpoll_imp_lepoll)
+apply (rule well_ord_Memrel [THEN well_ord_InfCard_square_eq], assumption)
+apply (rule Inf_Ord_imp_InfCard_cardinal, assumption+)
 done
 
 lemma Un_eqpoll_Inf_Ord:
-     "[| A \<approx> i; B \<approx> i; ~Finite(i); Ord(i) |] ==> A Un B \<approx> i"
+     "[| A \<approx> i; B \<approx> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<approx> i"
 apply (rule eqpollI)
-apply (blast intro: Un_lepoll_Inf_Ord_weak) 
-apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans]) 
-apply (rule Un_upper1 [THEN subset_imp_lepoll]) 
+apply (blast intro: Un_lepoll_Inf_Ord_weak)
+apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans])
+apply (rule Un_upper1 [THEN subset_imp_lepoll])
 done
 
 schematic_lemma paired_bij: "?f \<in> bij({{y,z}. y \<in> x}, x)"
@@ -79,19 +79,19 @@
 lemma paired_eqpoll: "{{y,z}. y \<in> x} \<approx> x"
 by (unfold eqpoll_def, fast intro!: paired_bij)
 
-lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B Int C = 0"
+lemma ex_eqpoll_disjoint: "\<exists>B. B \<approx> A & B \<inter> C = 0"
 by (fast intro!: paired_eqpoll equals0I elim: mem_asym)
 
 (*Finally we reach this result.  Surely there's a simpler proof, as sketched
   above?*)
 lemma Un_lepoll_Inf_Ord:
-     "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A Un B \<lesssim> i"
+     "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A \<union> B \<lesssim> i"
 apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE])
 apply (erule conjE)
-apply (drule lepoll_trans) 
+apply (drule lepoll_trans)
 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
 apply (rule Un_lepoll_Un [THEN lepoll_trans], (assumption+))
-apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll) 
+apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll)
 done
 
 lemma Least_in_Ord: "[| P(i); i \<in> j; Ord(j) |] ==> (LEAST i. P(i)) \<in> j"
@@ -103,14 +103,14 @@
 done
 
 lemma Diff_first_lepoll:
-     "[| well_ord(x,r); y \<subseteq> x; y \<lesssim> succ(n); n \<in> nat |] 
+     "[| well_ord(x,r); y \<subseteq> x; y \<lesssim> succ(n); n \<in> nat |]
       ==> y - {THE b. first(b,y,r)} \<lesssim> n"
-apply (case_tac "y=0", simp add: empty_lepollI) 
+apply (case_tac "y=0", simp add: empty_lepollI)
 apply (fast intro!: Diff_sing_lepoll the_first_in)
 done
 
 lemma UN_subset_split:
-     "(\<Union>x \<in> X. P(x)) \<subseteq> (\<Union>x \<in> X. P(x)-Q(x)) Un (\<Union>x \<in> X. Q(x))"
+     "(\<Union>x \<in> X. P(x)) \<subseteq> (\<Union>x \<in> X. P(x)-Q(x)) \<union> (\<Union>x \<in> X. Q(x))"
 by blast
 
 lemma UN_sing_lepoll: "Ord(a) ==> (\<Union>x \<in> a. {P(x)}) \<lesssim> a"
@@ -122,14 +122,14 @@
 done
 
 lemma UN_fun_lepoll_lemma [rule_format]:
-     "[| well_ord(T, R); ~Finite(a); Ord(a); n \<in> nat |] 
-      ==> \<forall>f. (\<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T) --> (\<Union>b \<in> a. f`b) \<lesssim> a"
+     "[| well_ord(T, R); ~Finite(a); Ord(a); n \<in> nat |]
+      ==> \<forall>f. (\<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T) \<longrightarrow> (\<Union>b \<in> a. f`b) \<lesssim> a"
 apply (induct_tac "n")
 apply (rule allI)
 apply (rule impI)
 apply (rule_tac b = "\<Union>b \<in> a. f`b" in subst)
 apply (rule_tac [2] empty_lepollI)
-apply (rule equals0I [symmetric], clarify) 
+apply (rule equals0I [symmetric], clarify)
 apply (fast dest: lepoll_0_is_0 [THEN subst])
 apply (rule allI)
 apply (rule impI)
@@ -137,19 +137,19 @@
 apply (erule impE, simp)
 apply (fast intro!: Diff_first_lepoll, simp)
 apply (rule UN_subset_split [THEN subset_imp_lepoll, THEN lepoll_trans])
-apply (fast intro: Un_lepoll_Inf_Ord UN_sing_lepoll) 
+apply (fast intro: Un_lepoll_Inf_Ord UN_sing_lepoll)
 done
 
 lemma UN_fun_lepoll:
-     "[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R);   
+     "[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R);
          ~Finite(a); Ord(a); n \<in> nat |] ==> (\<Union>b \<in> a. f`b) \<lesssim> a"
-by (blast intro: UN_fun_lepoll_lemma) 
+by (blast intro: UN_fun_lepoll_lemma)
 
 lemma UN_lepoll:
-     "[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R);   
-         ~Finite(a); Ord(a); n \<in> nat |] 
+     "[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R);
+         ~Finite(a); Ord(a); n \<in> nat |]
       ==> (\<Union>b \<in> a. F(b)) \<lesssim> a"
-apply (rule rev_mp) 
+apply (rule rev_mp)
 apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll)
 apply auto
 done
@@ -167,11 +167,11 @@
 apply (blast intro: Ord_Least ltI)
 done
 
-lemma lepoll_imp_eqpoll_subset: 
+lemma lepoll_imp_eqpoll_subset:
      "a \<lesssim> X ==> \<exists>Y. Y \<subseteq> X & a \<approx> Y"
-apply (unfold lepoll_def eqpoll_def, clarify) 
+apply (unfold lepoll_def eqpoll_def, clarify)
 apply (blast intro: restrict_bij
-             dest: inj_is_fun [THEN fun_is_rel, THEN image_subset]) 
+             dest: inj_is_fun [THEN fun_is_rel, THEN image_subset])
 done
 
 (* ********************************************************************** *)
@@ -184,27 +184,27 @@
 apply (frule_tac j=xa in Un_upper1_le [OF lt_Ord lt_Ord], assumption)
 apply (frule_tac j=xa in Un_upper2_le [OF lt_Ord lt_Ord], assumption)
 apply (drule Un_least_lt, assumption)
-apply (drule eqpoll_imp_lepoll [THEN lepoll_trans], 
+apply (drule eqpoll_imp_lepoll [THEN lepoll_trans],
        rule le_imp_lepoll, assumption)+
-apply (case_tac "Finite(x Un xa)")
+apply (case_tac "Finite(x \<union> xa)")
 txt{*finite case*}
- apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+) 
+ apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+)
  apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite])
  apply (fast dest: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_Finite])
 txt{*infinite case*}
 apply (drule Un_lepoll_Inf_Ord, (assumption+))
-apply (blast intro: le_Ord2) 
-apply (drule lesspoll_trans1 
-             [OF subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_trans] 
+apply (blast intro: le_Ord2)
+apply (drule lesspoll_trans1
+             [OF subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_trans]
                  lt_Card_imp_lesspoll], assumption+)
-apply (simp add: lesspoll_def) 
+apply (simp add: lesspoll_def)
 done
 
 lemma Diff_lesspoll_eqpoll_Card:
      "[| A \<approx> a; ~Finite(a); Card(a); B \<prec> a |] ==> A - B \<approx> a"
 apply (rule ccontr)
 apply (rule Diff_lesspoll_eqpoll_Card_lemma, (assumption+))
-apply (blast intro: lesspoll_def [THEN def_imp_iff, THEN iffD2] 
+apply (blast intro: lesspoll_def [THEN def_imp_iff, THEN iffD2]
                     subset_imp_lepoll eqpoll_imp_lepoll lepoll_trans)
 done
 
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/DC.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -82,13 +82,13 @@
 definition
   DC  :: "i => o"  where
     "DC(a) == \<forall>X R. R \<subseteq> Pow(X)*X  &
-                    (\<forall>Y \<in> Pow(X). Y \<prec> a --> (\<exists>x \<in> X. <Y,x> \<in> R)) 
-                    --> (\<exists>f \<in> a->X. \<forall>b<a. <f``b,f`b> \<in> R)"
+                    (\<forall>Y \<in> Pow(X). Y \<prec> a \<longrightarrow> (\<exists>x \<in> X. <Y,x> \<in> R)) 
+                    \<longrightarrow> (\<exists>f \<in> a->X. \<forall>b<a. <f``b,f`b> \<in> R)"
 
 definition
   DC0 :: o  where
     "DC0 == \<forall>A B R. R \<subseteq> A*B & R\<noteq>0 & range(R) \<subseteq> domain(R) 
-                    --> (\<exists>f \<in> nat->domain(R). \<forall>n \<in> nat. <f`n,f`succ(n)>:R)"
+                    \<longrightarrow> (\<exists>f \<in> nat->domain(R). \<forall>n \<in> nat. <f`n,f`succ(n)>:R)"
 
 definition
   ff  :: "[i, i, i, i] => i"  where
@@ -99,7 +99,7 @@
 locale DC0_imp =
   fixes XX and RR and X and R
 
-  assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat --> (\<exists>x \<in> X. <Y, x> \<in> R)"
+  assumes all_ex: "\<forall>Y \<in> Pow(X). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R)"
 
   defines XX_def: "XX == (\<Union>n \<in> nat. {f \<in> n->X. \<forall>k \<in> n. <f``k, f`k> \<in> R})"
      and RR_def:  "RR == {<z1,z2>:XX*XX. domain(z2)=succ(domain(z1))  
@@ -314,7 +314,7 @@
 lemma (in imp_DC0) lemma4:
      "[| range(R) \<subseteq> domain(R);  x \<in> domain(R) |]   
       ==> RR \<subseteq> Pow(XX)*XX &   
-             (\<forall>Y \<in> Pow(XX). Y \<prec> nat --> (\<exists>x \<in> XX. <Y,x>:RR))"
+             (\<forall>Y \<in> Pow(XX). Y \<prec> nat \<longrightarrow> (\<exists>x \<in> XX. <Y,x>:RR))"
 apply (rule conjI)
 apply (force dest!: FinD [THEN PowI] simp add: RR_def)
 apply (rule impI [THEN ballI])
@@ -331,7 +331,7 @@
 
 lemma (in imp_DC0) UN_image_succ_eq:
      "[| f \<in> nat->X; n \<in> nat |] 
-      ==> (\<Union>x \<in> f``succ(n). P(x)) =  P(f`n) Un (\<Union>x \<in> f``n. P(x))"
+      ==> (\<Union>x \<in> f``succ(n). P(x)) =  P(f`n) \<union> (\<Union>x \<in> f``n. P(x))"
 by (simp add: image_fun OrdmemD) 
 
 lemma (in imp_DC0) UN_image_succ_eq_succ:
@@ -475,7 +475,7 @@
 done
 
 (* ********************************************************************** *)
-(* \<forall>K. Card(K) --> DC(K) ==> WO3                                       *)
+(* \<forall>K. Card(K) \<longrightarrow> DC(K) ==> WO3                                       *)
 (* ********************************************************************** *)
 
 lemma fun_Ord_inj:
@@ -492,7 +492,7 @@
 lemma value_in_image: "[| f \<in> X->Y; A \<subseteq> X; a \<in> A |] ==> f`a \<in> f``A"
 by (fast elim!: image_fun [THEN ssubst])
 
-theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
+theorem DC_WO3: "(\<forall>K. Card(K) \<longrightarrow> DC(K)) ==> WO3"
 apply (unfold DC_def WO3_def)
 apply (rule allI)
 apply (case_tac "A \<prec> Hartog (A)")
@@ -516,7 +516,7 @@
 done
 
 (* ********************************************************************** *)
-(* WO1 ==> \<forall>K. Card(K) --> DC(K)                                       *)
+(* WO1 ==> \<forall>K. Card(K) \<longrightarrow> DC(K)                                       *)
 (* ********************************************************************** *)
 
 lemma images_eq:
@@ -538,7 +538,7 @@
 by (fast intro!: lam_type RepFunI)
 
 lemma lemmaX:
-     "[| \<forall>Y \<in> Pow(X). Y \<prec> K --> (\<exists>x \<in> X. <Y, x> \<in> R);   
+     "[| \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R);   
          b \<in> K; Z \<in> Pow(X); Z \<prec> K |]   
       ==> {x \<in> X. <Z,x> \<in> R} \<noteq> 0"
 by blast
@@ -546,7 +546,7 @@
 
 lemma WO1_DC_lemma:
      "[| Card(K); well_ord(X,Q);   
-         \<forall>Y \<in> Pow(X). Y \<prec> K --> (\<exists>x \<in> X. <Y, x> \<in> R); b \<in> K |]   
+         \<forall>Y \<in> Pow(X). Y \<prec> K \<longrightarrow> (\<exists>x \<in> X. <Y, x> \<in> R); b \<in> K |]   
       ==> ff(b, X, Q, R) \<in> {x \<in> X. <(\<lambda>c \<in> b. ff(c, X, Q, R))``b, x> \<in> R}"
 apply (rule_tac P = "b \<in> K" in impE, (erule_tac [2] asm_rl)+)
 apply (rule_tac i=b in Card_is_Ord [THEN Ord_in_Ord, THEN trans_induct], 
@@ -560,7 +560,7 @@
 apply (blast intro: lesspoll_trans1 in_Card_imp_lesspoll RepFun_lepoll)
 done
 
-theorem WO1_DC_Card: "WO1 ==> \<forall>K. Card(K) --> DC(K)"
+theorem WO1_DC_Card: "WO1 ==> \<forall>K. Card(K) \<longrightarrow> DC(K)"
 apply (unfold DC_def WO1_def)
 apply (rule allI impI)+
 apply (erule allE exE conjE)+
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/Hartog.thy
--- a/src/ZF/AC/Hartog.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/Hartog.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -12,7 +12,7 @@
   Hartog :: "i => i"  where
    "Hartog(X) == LEAST i. ~ i \<lesssim> X"
 
-lemma Ords_in_set: "\<forall>a. Ord(a) --> a \<in> X ==> P"
+lemma Ords_in_set: "\<forall>a. Ord(a) \<longrightarrow> a \<in> X ==> P"
 apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format])
 apply fast
 done
@@ -43,15 +43,15 @@
 done
 
 lemma Ords_lepoll_set_lemma:
-     "(\<forall>a. Ord(a) --> a \<lesssim> X) ==>   
-       \<forall>a. Ord(a) -->   
+     "(\<forall>a. Ord(a) \<longrightarrow> a \<lesssim> X) ==>   
+       \<forall>a. Ord(a) \<longrightarrow>   
         a \<in> {b. Z \<in> Pow(X)*Pow(X*X), \<exists>Y R. Z=<Y,R> & ordertype(Y,R)=b}"
 apply (intro allI impI)
 apply (elim allE impE, assumption)
 apply (blast dest!: Ord_lepoll_imp_eq_ordertype intro: sym) 
 done
 
-lemma Ords_lepoll_set: "\<forall>a. Ord(a) --> a \<lesssim> X ==> P"
+lemma Ords_lepoll_set: "\<forall>a. Ord(a) \<longrightarrow> a \<lesssim> X ==> P"
 by (erule Ords_lepoll_set_lemma [THEN Ords_in_set])
 
 lemma ex_Ord_not_lepoll: "\<exists>a. Ord(a) & ~a \<lesssim> X"
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/WO1_AC.thy
--- a/src/ZF/AC/WO1_AC.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO1_AC.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -11,7 +11,7 @@
 Assume WO1.  Let s be a set of infinite sets.
  
 Suppose x \<in> s.  Then x is equipollent to |x| (by WO1), an infinite cardinal
-call it K.  Since K = K |+| K = |K+K| (by InfCard_cdouble_eq) there is an 
+call it K.  Since K = K \<oplus> K = |K+K| (by InfCard_cdouble_eq) there is an 
 isomorphism h \<in> bij(K+K, x).  (Here + means disjoint sum.)
  
 So there is a partition of x into 2-element sets, namely
@@ -41,7 +41,7 @@
 
 lemma lemma1: "[| WO1; \<forall>B \<in> A. \<exists>C \<in> D(B). P(C,B) |] ==> \<exists>f. \<forall>B \<in> A. P(f`B,B)"
 apply (unfold WO1_def)
-apply (erule_tac x = "Union ({{C \<in> D (B) . P (C,B) }. B \<in> A}) " in allE)
+apply (erule_tac x = "\<Union>({{C \<in> D (B) . P (C,B) }. B \<in> A}) " in allE)
 apply (erule exE, drule ex_choice_fun, fast)
 apply (erule exE)
 apply (rule_tac x = "\<lambda>x \<in> A. f`{C \<in> D (x) . P (C,x) }" in exI)
@@ -82,7 +82,7 @@
 done
 
 lemma lemma2_5: 
-     "f \<in> bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i \<in> D})=B"
+     "f \<in> bij(D+D, B) ==> \<Union>({{f`Inl(i), f`Inr(i)}. i \<in> D})=B"
 apply (unfold bij_def surj_def)
 apply (fast elim!: inj_is_fun [THEN apply_type])
 done
@@ -91,7 +91,7 @@
      "[| WO1; ~Finite(B); 1\<le>n  |]   
       ==> \<exists>C \<in> Pow(Pow(B)). pairwise_disjoint(C) &   
                 sets_of_size_between(C, 2, succ(n)) &   
-                Union(C)=B"
+                \<Union>(C)=B"
 apply (drule lemma2_1 [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]], 
        assumption)
 apply (blast intro!: lemma2_2 lemma2_3 lemma2_4 lemma2_5)
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/WO1_WO7.thy
--- a/src/ZF/AC/WO1_WO7.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO1_WO7.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -2,10 +2,10 @@
     Author:     Lawrence C Paulson, CU Computer Laboratory
     Copyright   1998  University of Cambridge
 
-WO7 <-> LEMMA <-> WO1 (Rubin & Rubin p. 5)
+WO7 \<longleftrightarrow> LEMMA \<longleftrightarrow> WO1 (Rubin & Rubin p. 5)
 LEMMA is the sentence denoted by (**)
 
-Also, WO1 <-> WO8
+Also, WO1 \<longleftrightarrow> WO8
 *)
 
 theory WO1_WO7
@@ -14,13 +14,13 @@
 
 definition
     "LEMMA ==
-     \<forall>X. ~Finite(X) --> (\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"
+     \<forall>X. ~Finite(X) \<longrightarrow> (\<exists>R. well_ord(X,R) & ~well_ord(X,converse(R)))"
 
 (* ********************************************************************** *)
 (* It is easy to see that WO7 is equivalent to (**)                       *)
 (* ********************************************************************** *)
 
-lemma WO7_iff_LEMMA: "WO7 <-> LEMMA"
+lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA"
 apply (unfold WO7_def LEMMA_def)
 apply (blast intro: Finite_well_ord_converse)
 done
@@ -85,7 +85,7 @@
                     lepoll_def [THEN def_imp_iff, THEN iffD2] )
 done
 
-lemma WO1_iff_WO7: "WO1 <-> WO7"
+lemma WO1_iff_WO7: "WO1 \<longleftrightarrow> WO7"
 apply (simp add: WO7_iff_LEMMA)
 apply (blast intro: LEMMA_imp_WO1 WO1_imp_LEMMA)
 done
@@ -93,7 +93,7 @@
 
 
 (* ********************************************************************** *)
-(*            The proof of WO8 <-> WO1 (Rubin & Rubin p. 6)               *)
+(*            The proof of WO8 \<longleftrightarrow> WO1 (Rubin & Rubin p. 6)               *)
 (* ********************************************************************** *)
 
 lemma WO1_WO8: "WO1 ==> WO8"
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/WO2_AC16.thy
--- a/src/ZF/AC/WO2_AC16.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO2_AC16.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -9,7 +9,7 @@
 The first instance is trivial, the third not difficult, but the second
 is very complicated requiring many lemmas.
 We also need to prove that at any stage gamma the set 
-(s - Union(...) - k_gamma)   (Rubin & Rubin page 15)
+(s - \<Union>(...) - k_gamma)   (Rubin & Rubin page 15)
 contains m distinct elements (in fact is equipollent to s)
 *)
 
@@ -22,8 +22,8 @@
     "recfunAC16(f,h,i,a) == 
          transrec2(i, 0, 
               %g r. if (\<exists>y \<in> r. h`g \<subseteq> y) then r
-                    else r Un {f`(LEAST i. h`g \<subseteq> f`i & 
-                         (\<forall>b<a. (h`b \<subseteq> f`i --> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})"
+                    else r \<union> {f`(LEAST i. h`g \<subseteq> f`i & 
+                         (\<forall>b<a. (h`b \<subseteq> f`i \<longrightarrow> (\<forall>t \<in> r. ~ h`b \<subseteq> t))))})"
 
 (* ********************************************************************** *)
 (* Basic properties of recfunAC16                                         *)
@@ -35,10 +35,10 @@
 lemma recfunAC16_succ: 
      "recfunAC16(f,h,succ(i),a) =   
       (if (\<exists>y \<in> recfunAC16(f,h,i,a). h ` i \<subseteq> y) then recfunAC16(f,h,i,a)  
-       else recfunAC16(f,h,i,a) Un  
+       else recfunAC16(f,h,i,a) \<union>  
             {f ` (LEAST j. h ` i \<subseteq> f ` j &   
              (\<forall>b<a. (h`b \<subseteq> f`j   
-              --> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
+              \<longrightarrow> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
 apply (simp add: recfunAC16_def)
 done
 
@@ -52,7 +52,7 @@
 
 lemma transrec2_mono_lemma [rule_format]:
      "[| !!g r. r \<subseteq> B(g,r);  Ord(i) |]   
-      ==> j<i --> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
+      ==> j<i \<longrightarrow> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
 apply (erule trans_induct)
 apply (rule Ord_cases, assumption+, fast)
 apply (simp (no_asm_simp))
@@ -86,8 +86,8 @@
 
 
 lemma lemma3_1:
-    "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) --> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
-        \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j); j\<le>i; i<x; z<a;
+    "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
+        \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); j\<le>i; i<x; z<a;
         V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]   
      ==> V = W"
 apply (erule asm_rl allE impE)+
@@ -96,8 +96,8 @@
 
 
 lemma lemma3:
-    "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) --> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
-        \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j); i<x; j<x; z<a;   
+    "[| \<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) & f(z)<=Y);
+        \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); i<x; j<x; z<a;   
         V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]   
      ==> V = W"
 apply (rule_tac j=j in Ord_linear_le [OF lt_Ord lt_Ord], assumption+)
@@ -107,10 +107,10 @@
 
 lemma lemma4:
      "[| \<forall>y<x. F(y) \<subseteq> X &   
-                (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) -->   
+                (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>   
                  (\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y)); 
          x < a |]   
-      ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) -->   
+      ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) \<longrightarrow>   
                        (\<exists>! Y. Y \<in> F(y) & h(z) \<subseteq> Y)"
 apply (intro oallI impI)
 apply (drule ospec, assumption, clarify)
@@ -119,12 +119,12 @@
 
 lemma lemma5:
      "[| \<forall>y<x. F(y) \<subseteq> X &   
-               (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) -->   
+               (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>   
                 (\<exists>! Y. Y \<in> F(y) & h(x) \<subseteq> Y));  
-         x < a; Limit(x); \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j) |]   
+         x < a; Limit(x); \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |]   
       ==> (\<Union>x<x. F(x)) \<subseteq> X &   
           (\<forall>xa<a. xa < x | (\<exists>x \<in> \<Union>x<x. F(x). h(xa) \<subseteq> x)   
-                --> (\<exists>! Y. Y \<in> (\<Union>x<x. F(x)) & h(xa) \<subseteq> Y))"
+                \<longrightarrow> (\<exists>! Y. Y \<in> (\<Union>x<x. F(x)) & h(xa) \<subseteq> Y))"
 apply (rule conjI)
 apply (rule subsetI)
 apply (erule OUN_E)
@@ -147,7 +147,7 @@
 (*
   First quite complicated proof of the fact used in the recursive construction
   of the family T_gamma (WO2 ==> AC16(k #+ m, k)) - the fact that at any stage
-  gamma the set (s - Union(...) - k_gamma) is equipollent to s
+  gamma the set (s - \<Union>(...) - k_gamma) is equipollent to s
   (Rubin & Rubin page 15).
 *)
 
@@ -179,7 +179,7 @@
 lemma Union_lesspoll:
      "[| \<forall>x \<in> X. x lepoll n & x \<subseteq> T; well_ord(T, R); X lepoll b;   
          b<a; ~Finite(a); Card(a); n \<in> nat |]   
-      ==> Union(X)\<prec>a"
+      ==> \<Union>(X)\<prec>a"
 apply (case_tac "Finite (X)")
 apply (blast intro: Card_is_Ord Finite_lesspoll_infinite_Ord 
                     lepoll_nat_imp_Finite Finite_Union)
@@ -200,10 +200,10 @@
 (* recfunAC16_lepoll_index                                                *)
 (* ********************************************************************** *)
 
-lemma Un_sing_eq_cons: "A Un {a} = cons(a, A)"
+lemma Un_sing_eq_cons: "A \<union> {a} = cons(a, A)"
 by fast
 
-lemma Un_lepoll_succ: "A lepoll B ==> A Un {a} lepoll succ(B)"
+lemma Un_lepoll_succ: "A lepoll B ==> A \<union> {a} lepoll succ(B)"
 apply (simp add: Un_sing_eq_cons succ_def)
 apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
 done
@@ -211,7 +211,7 @@
 lemma Diff_UN_succ_empty: "Ord(a) ==> F(a) - (\<Union>b<succ(a). F(b)) = 0"
 by (fast intro!: le_refl)
 
-lemma Diff_UN_succ_subset: "Ord(a) ==> F(a) Un X - (\<Union>b<succ(a). F(b)) \<subseteq> X"
+lemma Diff_UN_succ_subset: "Ord(a) ==> F(a) \<union> X - (\<Union>b<succ(a). F(b)) \<subseteq> X"
 by blast
 
 lemma recfunAC16_Diff_lepoll_1:
@@ -288,7 +288,7 @@
 lemma Union_recfunAC16_lesspoll:
      "[| recfunAC16(f,g,y,a) \<subseteq> {X \<in> Pow(A). X\<approx>n};   
          A\<approx>a;  y<a;  ~Finite(a);  Card(a);  n \<in> nat |]   
-      ==> Union(recfunAC16(f,g,y,a))\<prec>a"
+      ==> \<Union>(recfunAC16(f,g,y,a))\<prec>a"
 apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE])
 apply (rule_tac T=A in Union_lesspoll, simp_all)
 apply (blast intro!: eqpoll_imp_lepoll)
@@ -302,7 +302,7 @@
          Card(a); ~ Finite(a); A\<approx>a;   
          k \<in> nat;  y<a;   
          h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)}) |]   
-      ==> A - Union(recfunAC16(f, h, y, a)) - h`y\<approx>a"
+      ==> A - \<Union>(recfunAC16(f, h, y, a)) - h`y\<approx>a"
 apply (rule dbl_Diff_eqpoll_Card, simp_all)
 apply (simp add: Union_recfunAC16_lesspoll)
 apply (rule Finite_lesspoll_infinite_Ord) 
@@ -320,7 +320,7 @@
 
 lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;   
         h \<in> bij(a, {x \<in> Pow(A) . x\<approx>k}); i<a; k \<in> nat; m \<in> nat |]   
-        ==> h ` i Un x \<in> {x \<in> Pow(A) . x\<approx>k #+ m}"
+        ==> h ` i \<union> x \<in> {x \<in> Pow(A) . x\<approx>k #+ m}"
 by (blast intro: disj_Un_eqpoll_nat_sum
           dest:  ltD bij_is_fun [THEN apply_type])
 
@@ -330,14 +330,14 @@
 (* ********************************************************************** *)
 
 lemma lemma6:
-     "[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) --> Q(x,y)); succ(j)<a |]
-      ==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) --> Q(x,j))"
+     "[| \<forall>y<succ(j). F(y)<=X & (\<forall>x<a. x<y | P(x,y) \<longrightarrow> Q(x,y)); succ(j)<a |]
+      ==> F(j)<=X & (\<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j))"
 by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]) 
 
 
 lemma lemma7:
-     "[| \<forall>x<a. x<j | P(x,j) --> Q(x,j);  succ(j)<a |]   
-      ==> P(j,j) --> (\<forall>x<a. x\<le>j | P(x,j) --> Q(x,j))"
+     "[| \<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j);  succ(j)<a |]   
+      ==> P(j,j) \<longrightarrow> (\<forall>x<a. x\<le>j | P(x,j) \<longrightarrow> Q(x,j))"
 by (fast elim!: leE)
 
 (* ********************************************************************** *)
@@ -354,12 +354,12 @@
 apply (fast elim!: eqpoll_sym)
 done
 
-lemma subset_Un_disjoint: "[| A \<subseteq> B Un C; A Int C = 0 |] ==> A \<subseteq> B"
+lemma subset_Un_disjoint: "[| A \<subseteq> B \<union> C; A \<inter> C = 0 |] ==> A \<subseteq> B"
 by blast
 
 
 lemma Int_empty:
-     "[| X \<in> Pow(A - Union(B) -C); T \<in> B; F \<subseteq> T |] ==> F Int X = 0"
+     "[| X \<in> Pow(A - \<Union>(B) -C); T \<in> B; F \<subseteq> T |] ==> F \<inter> X = 0"
 by blast
 
 
@@ -369,7 +369,7 @@
 
 
 lemma subset_imp_eq_lemma:
-     "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m lepoll A & B lepoll m --> A=B"
+     "m \<in> nat ==> \<forall>A B. A \<subseteq> B & m lepoll A & B lepoll m \<longrightarrow> A=B"
 apply (induct_tac "m")
 apply (fast dest!: lepoll_0_is_0)
 apply (intro allI impI)
@@ -407,7 +407,7 @@
          h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)});   
          ~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |]   
       ==> \<exists>X \<in> {Y \<in> Pow(A). Y\<approx>succ(k #+ m)}. h`y \<subseteq> X &   
-                (\<forall>b<a. h`b \<subseteq> X -->   
+                (\<forall>b<a. h`b \<subseteq> X \<longrightarrow>   
                 (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))"
 apply (erule_tac m1=m in dbl_Diff_eqpoll [THEN ex_subset_eqpoll, THEN bexE], 
        assumption+)
@@ -434,7 +434,7 @@
          f \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k #+ m)});   
          ~ (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y) |]   
       ==> \<exists>c<a. h`y \<subseteq> f`c &   
-                (\<forall>b<a. h`b \<subseteq> f`c -->   
+                (\<forall>b<a. h`b \<subseteq> f`c \<longrightarrow>   
                 (\<forall>T \<in> recfunAC16(f, h, y, a). ~ h`b \<subseteq> T))"
 apply (drule ex_next_set, assumption+)
 apply (erule bexE)
@@ -451,11 +451,11 @@
 
 lemma lemma8:
      "[| \<forall>x<a. x<j | (\<exists>xa \<in> F(j). P(x, xa))   
-         --> (\<exists>! Y. Y \<in> F(j) & P(x, Y)); F(j) \<subseteq> X;   
-         L \<in> X; P(j, L) & (\<forall>x<a. P(x, L) --> (\<forall>xa \<in> F(j). ~P(x, xa))) |]   
-      ==> F(j) Un {L} \<subseteq> X &   
-          (\<forall>x<a. x\<le>j | (\<exists>xa \<in> (F(j) Un {L}). P(x, xa)) -->   
-                 (\<exists>! Y. Y \<in> (F(j) Un {L}) & P(x, Y)))"
+         \<longrightarrow> (\<exists>! Y. Y \<in> F(j) & P(x, Y)); F(j) \<subseteq> X;   
+         L \<in> X; P(j, L) & (\<forall>x<a. P(x, L) \<longrightarrow> (\<forall>xa \<in> F(j). ~P(x, xa))) |]   
+      ==> F(j) \<union> {L} \<subseteq> X &   
+          (\<forall>x<a. x\<le>j | (\<exists>xa \<in> (F(j) \<union> {L}). P(x, xa)) \<longrightarrow>   
+                 (\<exists>! Y. Y \<in> (F(j) \<union> {L}) & P(x, Y)))"
 apply (rule conjI)
 apply (fast intro!: singleton_subsetI)
 apply (rule oallI)
@@ -472,7 +472,7 @@
          h \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k)});   
          ~Finite(a); Card(a); A\<approx>a; k \<in> nat; m \<in> nat |]   
       ==> recfunAC16(f, h, b, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)} &   
-          (\<forall>x<a. x < b | (\<exists>Y \<in> recfunAC16(f, h, b, a). h ` x \<subseteq> Y) -->   
+          (\<forall>x<a. x < b | (\<exists>Y \<in> recfunAC16(f, h, b, a). h ` x \<subseteq> Y) \<longrightarrow>   
           (\<exists>! Y. Y \<in> recfunAC16(f, h, b, a) & h ` x \<subseteq> Y))"
 apply (erule lt_induct)
 apply (frule lt_Ord)
@@ -507,10 +507,10 @@
 (* ********************************************************************** *)
 
 lemma lemma_simp_induct:
-     "[| \<forall>b. b<a --> F(b) \<subseteq> S & (\<forall>x<a. (x<b | (\<exists>Y \<in> F(b). f`x \<subseteq> Y))  
-                                   --> (\<exists>! Y. Y \<in> F(b) & f`x \<subseteq> Y));
+     "[| \<forall>b. b<a \<longrightarrow> F(b) \<subseteq> S & (\<forall>x<a. (x<b | (\<exists>Y \<in> F(b). f`x \<subseteq> Y))  
+                                   \<longrightarrow> (\<exists>! Y. Y \<in> F(b) & f`x \<subseteq> Y));
          f \<in> a->f``(a); Limit(a); 
-         \<forall>i j. i\<le>j --> F(i) \<subseteq> F(j) |]   
+         \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j) |]   
         ==> (\<Union>j<a. F(j)) \<subseteq> S &   
             (\<forall>x \<in> f``a. \<exists>! Y. Y \<in> (\<Union>j<a. F(j)) & x \<subseteq> Y)"
 apply (rule conjI)
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/AC/WO6_WO1.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -22,7 +22,7 @@
   
 definition
   uu  :: "[i, i, i, i] => i"  where
-    "uu(f, beta, gamma, delta) == (f`beta * f`gamma) Int f`delta"
+    "uu(f, beta, gamma, delta) == (f`beta * f`gamma) \<inter> f`delta"
 
 
 (** Definitions for case 1 **)
@@ -171,9 +171,9 @@
 (* ********************************************************************** *)
 lemma cases: 
      "\<forall>b<a. \<forall>g<a. \<forall>d<a. u(f,b,g,d) \<lesssim> m   
-      ==> (\<forall>b<a. f`b \<noteq> 0 -->  
+      ==> (\<forall>b<a. f`b \<noteq> 0 \<longrightarrow>  
                   (\<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 & u(f,b,g,d) \<prec> m))  
-        | (\<exists>b<a. f`b \<noteq> 0 & (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 -->   
+        | (\<exists>b<a. f`b \<noteq> 0 & (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow>   
                                         u(f,b,g,d) \<approx> m))"
 apply (unfold lesspoll_def)
 apply (blast del: equalityI)
@@ -182,7 +182,7 @@
 (* ********************************************************************** *)
 (* Lemmas used in both cases                                              *)
 (* ********************************************************************** *)
-lemma UN_oadd: "Ord(a) ==> (\<Union>b<a++a. C(b)) = (\<Union>b<a. C(b) Un C(a++b))"
+lemma UN_oadd: "Ord(a) ==> (\<Union>b<a++a. C(b)) = (\<Union>b<a. C(b) \<union> C(a++b))"
 by (blast intro: ltI lt_oadd1 oadd_lt_mono2 dest!: lt_oadd_disj)
 
 
@@ -223,7 +223,7 @@
 
 lemma gg1_lepoll_m: 
      "[| Ord(a);  m \<in> nat;   
-         \<forall>b<a. f`b \<noteq>0 -->                                        
+         \<forall>b<a. f`b \<noteq>0 \<longrightarrow>                                        
              (\<exists>g<a. \<exists>d<a. domain(uu(f,b,g,d)) \<noteq> 0  &                
                           domain(uu(f,b,g,d)) \<lesssim> m);             
          \<forall>b<a. f`b \<lesssim> succ(m);  b<a++a |] 
@@ -293,7 +293,7 @@
 done
 
 lemma uu_Least_is_fun:
-     "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 -->                
+     "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow>                
           domain(uu(f, b, g, d)) \<approx> succ(m);                         
           \<forall>b<a. f`b \<lesssim> succ(m);  y*y \<subseteq> y;                        
           (\<Union>b<a. f`b)=y;  b<a;  g<a;  d<a;                             
@@ -312,7 +312,7 @@
 done
 
 lemma vv2_subset: 
-     "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 -->             
+     "[| \<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow>             
                        domain(uu(f, b, g, d)) \<approx> succ(m);
          \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
          (\<Union>b<a. f`b)=y;  b<a;  g<a;  m \<in> nat;  s \<in> f`b |] 
@@ -325,7 +325,7 @@
 (* Case 2: Union of images is the whole "y"                              *)
 (* ********************************************************************** *)
 lemma UN_gg2_eq: 
-     "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 -->              
+     "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow>              
                domain(uu(f,b,g,d)) \<approx> succ(m);                         
          \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;                        
          (\<Union>b<a. f`b)=y;  Ord(a);  m \<in> nat;  s \<in> f`b;  b<a |] 
@@ -366,7 +366,7 @@
 done
 
 lemma gg2_lepoll_m: 
-     "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 -->              
+     "[| \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow>              
                       domain(uu(f,b,g,d)) \<approx> succ(m);                         
          \<forall>b<a. f`b \<lesssim> succ(m);  y*y \<subseteq> y;                     
          (\<Union>b<a. f`b)=y;  b<a;  s \<in> f`b;  m \<in> nat;  m\<noteq> 0;  g<a++a |] 
@@ -401,7 +401,7 @@
 
 (* ********************************************************************** *)
 (* lemma iv - p. 4:                                                       *)
-(* For every set x there is a set y such that   x Un (y * y) \<subseteq> y         *)
+(* For every set x there is a set y such that   x \<union> (y * y) \<subseteq> y         *)
 (* ********************************************************************** *)
 
 
@@ -409,29 +409,29 @@
    (used only in the following two lemmas)                          *)
 
 lemma z_n_subset_z_succ_n:
-     "\<forall>n \<in> nat. rec(n, x, %k r. r Un r*r) \<subseteq> rec(succ(n), x, %k r. r Un r*r)"
+     "\<forall>n \<in> nat. rec(n, x, %k r. r \<union> r*r) \<subseteq> rec(succ(n), x, %k r. r \<union> r*r)"
 by (fast intro: rec_succ [THEN ssubst])
 
 lemma le_subsets:
      "[| \<forall>n \<in> nat. f(n)<=f(succ(n)); n\<le>m; n \<in> nat; m \<in> nat |]   
       ==> f(n)<=f(m)"
 apply (erule_tac P = "n\<le>m" in rev_mp)
-apply (rule_tac P = "%z. n\<le>z --> f (n) \<subseteq> f (z) " in nat_induct) 
+apply (rule_tac P = "%z. n\<le>z \<longrightarrow> f (n) \<subseteq> f (z) " in nat_induct) 
 apply (auto simp add: le_iff) 
 done
 
 lemma le_imp_rec_subset:
      "[| n\<le>m; m \<in> nat |] 
-      ==> rec(n, x, %k r. r Un r*r) \<subseteq> rec(m, x, %k r. r Un r*r)"
+      ==> rec(n, x, %k r. r \<union> r*r) \<subseteq> rec(m, x, %k r. r \<union> r*r)"
 apply (rule z_n_subset_z_succ_n [THEN le_subsets])
 apply (blast intro: lt_nat_in_nat)+
 done
 
-lemma lemma_iv: "\<exists>y. x Un y*y \<subseteq> y"
-apply (rule_tac x = "\<Union>n \<in> nat. rec (n, x, %k r. r Un r*r) " in exI)
+lemma lemma_iv: "\<exists>y. x \<union> y*y \<subseteq> y"
+apply (rule_tac x = "\<Union>n \<in> nat. rec (n, x, %k r. r \<union> r*r) " in exI)
 apply safe
 apply (rule nat_0I [THEN UN_I], simp)
-apply (rule_tac a = "succ (n Un na) " in UN_I)
+apply (rule_tac a = "succ (n \<union> na) " in UN_I)
 apply (erule Un_nat_type [THEN nat_succI], assumption)
 apply (auto intro: le_imp_rec_subset [THEN subsetD] 
             intro!: Un_upper1_le Un_upper2_le Un_nat_type 
@@ -494,7 +494,7 @@
 
 lemma rev_induct_lemma [rule_format]: 
      "[| n \<in> nat; !!m. [| m \<in> nat; m\<noteq>0; P(succ(m)) |] ==> P(m) |]   
-      ==> n\<noteq>0 --> P(n) --> P(1)"
+      ==> n\<noteq>0 \<longrightarrow> P(n) \<longrightarrow> P(1)"
 by (erule nat_induct, blast+)
 
 lemma rev_induct:
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Coind/Dynamic.thy
--- a/src/ZF/Coind/Dynamic.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Dynamic.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -8,7 +8,7 @@
 consts
   EvalRel :: i
 inductive
-  domains "EvalRel" <= "ValEnv * Exp * Val"
+  domains "EvalRel" \<subseteq> "ValEnv * Exp * Val"
   intros
     eval_constI:
       " [| ve \<in> ValEnv; c \<in> Const |] ==>   
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/ECR.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -10,7 +10,7 @@
 consts
   HasTyRel :: i
 coinductive
-  domains "HasTyRel" <= "Val * Ty"
+  domains "HasTyRel" \<subseteq> "Val * Ty"
   intros
     htr_constI [intro!]:
       "[| c \<in> Const; t \<in> Ty; isof(c,t) |] ==> <v_const(c),t> \<in> HasTyRel"
@@ -37,7 +37,7 @@
      "[| x \<in> ExVar; e \<in> Exp; t \<in> Ty; ve \<in> ValEnv; te \<in> TyEnv;   
          <te, e_fn(x, e), t> \<in> ElabRel; ve_dom(ve) = te_dom(te);  
          {<ve_app(ve,y),te_app(te,y)>.y \<in> ve_dom(ve)} \<in>
-           Pow({<v_clos(x,e,ve),t>} Un HasTyRel) |]     
+           Pow({<v_clos(x,e,ve),t>} \<union> HasTyRel) |]     
       ==> <v_clos(x, e, ve),t> \<in> HasTyRel"
 apply (rule singletonI [THEN HasTyRel.coinduct], auto)
 done
@@ -113,10 +113,10 @@
  "[| ve \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; c1 \<in> Const; c2 \<in> Const;    
      <ve,e1,v_const(c1)> \<in> EvalRel;                       
      \<forall>t te.                                          
-       hastyenv(ve,te) --> <te,e1,t> \<in> ElabRel --> <v_const(c1),t> \<in> HasTyRel;
+       hastyenv(ve,te) \<longrightarrow> <te,e1,t> \<in> ElabRel \<longrightarrow> <v_const(c1),t> \<in> HasTyRel;
      <ve, e2, v_const(c2)> \<in> EvalRel;                   
      \<forall>t te.                                          
-       hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v_const(c2),t> \<in> HasTyRel;
+       hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v_const(c2),t> \<in> HasTyRel;
      hastyenv(ve, te);                                  
      <te,e_app(e1,e2),t> \<in> ElabRel |] 
   ==> <v_const(c_app(c1, c2)),t> \<in> HasTyRel"
@@ -126,13 +126,13 @@
  "[| ve \<in> ValEnv; vem \<in> ValEnv; e1 \<in> Exp; e2 \<in> Exp; em \<in> Exp; xm \<in> ExVar; 
      v \<in> Val;   
      <ve,e1,v_clos(xm,em,vem)> \<in> EvalRel;        
-     \<forall>t te. hastyenv(ve,te) -->                     
-            <te,e1,t> \<in> ElabRel --> <v_clos(xm,em,vem),t> \<in> HasTyRel;         
+     \<forall>t te. hastyenv(ve,te) \<longrightarrow>                     
+            <te,e1,t> \<in> ElabRel \<longrightarrow> <v_clos(xm,em,vem),t> \<in> HasTyRel;         
      <ve,e2,v2> \<in> EvalRel;                       
-     \<forall>t te. hastyenv(ve,te) --> <te,e2,t> \<in> ElabRel --> <v2,t> \<in> HasTyRel;
+     \<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e2,t> \<in> ElabRel \<longrightarrow> <v2,t> \<in> HasTyRel;
      <ve_owr(vem,xm,v2),em,v> \<in> EvalRel;         
-     \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) -->      
-            <te,em,t> \<in> ElabRel --> <v,t> \<in> HasTyRel;
+     \<forall>t te. hastyenv(ve_owr(vem,xm,v2),te) \<longrightarrow>      
+            <te,em,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel;
      hastyenv(ve,te); <te,e_app(e1,e2),t> \<in> ElabRel |] 
    ==> <v,t> \<in> HasTyRel"
 apply (erule elab_appE)
@@ -150,7 +150,7 @@
 
 lemma consistency [rule_format]:
    "<ve,e,v> \<in> EvalRel 
-    ==> (\<forall>t te. hastyenv(ve,te) --> <te,e,t> \<in> ElabRel --> <v,t> \<in> HasTyRel)"
+    ==> (\<forall>t te. hastyenv(ve,te) \<longrightarrow> <te,e,t> \<in> ElabRel \<longrightarrow> <v,t> \<in> HasTyRel)"
 apply (erule EvalRel.induct)
 apply (simp_all add: consistency_const consistency_var consistency_fn 
                      consistency_fix consistency_app1)
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Map.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -9,7 +9,7 @@
 
 definition
   TMap :: "[i,i] => i"  where
-   "TMap(A,B) == {m \<in> Pow(A*Union(B)).\<forall>a \<in> A. m``{a} \<in> B}"
+   "TMap(A,B) == {m \<in> Pow(A*\<Union>(B)).\<forall>a \<in> A. m``{a} \<in> B}"
 
 definition
   PMap :: "[i,i] => i"  where
@@ -23,24 +23,24 @@
 
 definition
   map_owr :: "[i,i,i]=>i"  where
-   "map_owr(m,a,b) == \<Sigma> x \<in> {a} Un domain(m). if x=a then b else m``{x}"
+   "map_owr(m,a,b) == \<Sigma> x \<in> {a} \<union> domain(m). if x=a then b else m``{x}"
 
 definition
   map_app :: "[i,i]=>i"  where
    "map_app(m,a) == m``{a}"
   
-lemma "{0,1} \<subseteq> {1} Un TMap(I, {0,1})"
+lemma "{0,1} \<subseteq> {1} \<union> TMap(I, {0,1})"
 by (unfold TMap_def, blast)
 
-lemma "{0} Un TMap(I,1) \<subseteq> {1} Un TMap(I, {0} Un TMap(I,1))"
+lemma "{0} \<union> TMap(I,1) \<subseteq> {1} \<union> TMap(I, {0} \<union> TMap(I,1))"
 by (unfold TMap_def, blast)
 
-lemma "{0,1} Un TMap(I,2) \<subseteq> {1} Un TMap(I, {0,1} Un TMap(I,2))"
+lemma "{0,1} \<union> TMap(I,2) \<subseteq> {1} \<union> TMap(I, {0,1} \<union> TMap(I,2))"
 by (unfold TMap_def, blast)
 
 (*A bit too slow.
-lemma "{0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2) \<subseteq>  
-       {1} Un TMap(I, {0,1} Un TMap(I,TMap(I,2)) Un TMap(I,2))"
+lemma "{0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2) \<subseteq>  
+       {1} \<union> TMap(I, {0,1} \<union> TMap(I,TMap(I,2)) \<union> TMap(I,2))"
 by (unfold TMap_def, blast)
 *)
 
@@ -68,7 +68,7 @@
 (* Lemmas *)
 
 lemma MapQU_lemma: 
-    "A \<subseteq> univ(X) ==> Pow(A * Union(quniv(X))) \<subseteq> quniv(X)"
+    "A \<subseteq> univ(X) ==> Pow(A * \<Union>(quniv(X))) \<subseteq> quniv(X)"
 apply (unfold quniv_def)
 apply (rule Pow_mono)
 apply (rule subset_trans [OF Sigma_mono product_univ])
@@ -164,7 +164,7 @@
 by (unfold map_emp_def, blast)
 
 lemma map_domain_owr: 
-  "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)"
+  "b \<noteq> 0 ==> domain(map_owr(f,a,b)) = {a} \<union> domain(f)"
 apply (unfold map_owr_def)
 apply (auto simp add: domain_Sigma)
 done
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Coind/Static.thy
--- a/src/ZF/Coind/Static.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Static.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -27,7 +27,7 @@
 consts  ElabRel :: i
 
 inductive
-  domains "ElabRel" <= "TyEnv * Exp * Ty"
+  domains "ElabRel" \<subseteq> "TyEnv * Exp * Ty"
   intros
     constI [intro!]:
       "[| te \<in> TyEnv; c \<in> Const; t \<in> Ty; isof(c,t) |] ==>   
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Types.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -30,7 +30,7 @@
 
 primrec (*domain of the type environment*)
   "te_dom (te_emp) = 0"
-  "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"
+  "te_dom (te_owr(te,x,v)) = te_dom(te) \<union> {x}"
 
 primrec (*lookup up identifiers in the type environment*)
   "te_app (te_emp,x) = 0"
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Values.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -80,7 +80,7 @@
 (* Equalities for value environments *)
 
 lemma ve_dom_owr [simp]:
-     "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"
+     "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) \<union> {x}"
 apply (erule ValEnvE)
 apply (auto simp add: map_domain_owr)
 done
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/IMP/Equiv.thy
--- a/src/ZF/IMP/Equiv.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/IMP/Equiv.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -8,7 +8,7 @@
 
 lemma aexp_iff [rule_format]:
   "[| a \<in> aexp; sigma: loc -> nat |] 
-    ==> ALL n. <a,sigma> -a-> n <-> A(a,sigma) = n"
+    ==> \<forall>n. <a,sigma> -a-> n \<longleftrightarrow> A(a,sigma) = n"
   apply (erule aexp.induct)
      apply (force intro!: evala.intros)+
   done
@@ -27,7 +27,7 @@
 
 lemma bexp_iff [rule_format]:
   "[| b \<in> bexp; sigma: loc -> nat |] 
-    ==> ALL w. <b,sigma> -b-> w <-> B(b,sigma) = w"
+    ==> \<forall>w. <b,sigma> -b-> w \<longleftrightarrow> B(b,sigma) = w"
   apply (erule bexp.induct) 
   apply (auto intro!: evalb.intros)
   done
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/Acc.thy
--- a/src/ZF/Induct/Acc.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Acc.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -36,7 +36,7 @@
 
 lemma acc_induct [consumes 1, case_names vimage, induct set: acc]:
     "[| a \<in> acc(r);
-        !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r --> P(y) |] ==> P(x)
+        !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x)
      |] ==> P(a)"
   by (erule acc.induct) (blast intro: acc.intros)
 
@@ -55,7 +55,7 @@
    apply (blast intro: accI)+
   done
 
-lemma wf_acc_iff: "wf(r) <-> field(r) \<subseteq> acc(r)"
+lemma wf_acc_iff: "wf(r) \<longleftrightarrow> field(r) \<subseteq> acc(r)"
   by (rule iffI, erule acc_wfD, erule acc_wfI)
 
 end
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Binary_Trees.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -20,7 +20,7 @@
 lemma Br_neq_left: "l \<in> bt(A) ==> Br(x, l, r) \<noteq> l"
   by (induct arbitrary: x r set: bt) auto
 
-lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
+lemma Br_iff: "Br(a, l, r) = Br(a', l', r') \<longleftrightarrow> a = a' & l = l' & r = r'"
   -- "Proving a freeness theorem."
   by (fast elim!: bt.free_elims)
 
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Comb.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -28,7 +28,7 @@
 
 text {*
   Inductive definition of contractions, @{text "-1->"} and
-  (multi-step) reductions, @{text "--->"}.
+  (multi-step) reductions, @{text "-\<longrightarrow>"}.
 *}
 
 consts
@@ -39,8 +39,8 @@
   where "p -1-> q == <p,q> \<in> contract"
 
 abbreviation
-  contract_multi :: "[i,i] => o"    (infixl "--->" 50)
-  where "p ---> q == <p,q> \<in> contract^*"
+  contract_multi :: "[i,i] => o"    (infixl "-\<longrightarrow>" 50)
+  where "p -\<longrightarrow> q == <p,q> \<in> contract^*"
 
 inductive
   domains "contract" \<subseteq> "comb \<times> comb"
@@ -87,14 +87,14 @@
 definition
   diamond :: "i => o"  where
   "diamond(r) ==
-    \<forall>x y. <x,y>\<in>r --> (\<forall>y'. <x,y'>\<in>r --> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
+    \<forall>x y. <x,y>\<in>r \<longrightarrow> (\<forall>y'. <x,y'>\<in>r \<longrightarrow> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
 
 
 subsection {* Transitive closure preserves the Church-Rosser property *}
 
 lemma diamond_strip_lemmaD [rule_format]:
   "[| diamond(r);  <x,y>:r^+ |] ==>
-    \<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
+    \<forall>y'. <x,y'>:r \<longrightarrow> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
   apply (unfold diamond_def)
   apply (erule trancl_induct)
    apply (blast intro: r_into_trancl)
@@ -145,7 +145,7 @@
   contract.Ap1 [THEN rtrancl_into_rtrancl2]
   contract.Ap2 [THEN rtrancl_into_rtrancl2]
 
-lemma "p \<in> comb ==> I\<bullet>p ---> p"
+lemma "p \<in> comb ==> I\<bullet>p -\<longrightarrow> p"
   -- {* Example only: not used *}
   by (unfold I_def) (blast intro: reduction_rls)
 
@@ -168,7 +168,7 @@
 lemma K1_contractD: "K\<bullet>p -1-> r ==> (\<exists>q. r = K\<bullet>q & p -1-> q)"
   by auto
 
-lemma Ap_reduce1: "[| p ---> q;  r \<in> comb |] ==> p\<bullet>r ---> q\<bullet>r"
+lemma Ap_reduce1: "[| p -\<longrightarrow> q;  r \<in> comb |] ==> p\<bullet>r -\<longrightarrow> q\<bullet>r"
   apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
   apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
   apply (erule rtrancl_induct)
@@ -177,7 +177,7 @@
   apply (blast intro: contract_combD2 reduction_rls)
   done
 
-lemma Ap_reduce2: "[| p ---> q;  r \<in> comb |] ==> r\<bullet>p ---> r\<bullet>q"
+lemma Ap_reduce2: "[| p -\<longrightarrow> q;  r \<in> comb |] ==> r\<bullet>p -\<longrightarrow> r\<bullet>q"
   apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
   apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
   apply (erule rtrancl_induct)
@@ -247,13 +247,13 @@
   done
 
 text {*
-  \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
+  \medskip Equivalence of @{prop "p -\<longrightarrow> q"} and @{prop "p ===> q"}.
 *}
 
 lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
   by (induct set: contract) auto
 
-lemma reduce_imp_parreduce: "p--->q ==> p===>q"
+lemma reduce_imp_parreduce: "p-\<longrightarrow>q ==> p===>q"
   apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
   apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
   apply (erule rtrancl_induct)
@@ -262,7 +262,7 @@
     trans_trancl [THEN transD])
   done
 
-lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
+lemma parcontract_imp_reduce: "p=1=>q ==> p-\<longrightarrow>q"
   apply (induct set: parcontract)
      apply (blast intro: reduction_rls)
     apply (blast intro: reduction_rls)
@@ -271,7 +271,7 @@
     Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
   done
 
-lemma parreduce_imp_reduce: "p===>q ==> p--->q"
+lemma parreduce_imp_reduce: "p===>q ==> p-\<longrightarrow>q"
   apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
   apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
   apply (erule trancl_induct, erule parcontract_imp_reduce)
@@ -279,7 +279,7 @@
   apply (erule parcontract_imp_reduce)
   done
 
-lemma parreduce_iff_reduce: "p===>q <-> p--->q"
+lemma parreduce_iff_reduce: "p===>q \<longleftrightarrow> p-\<longrightarrow>q"
   by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)
 
 end
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/FoldSet.thy
--- a/src/ZF/Induct/FoldSet.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/FoldSet.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -11,10 +11,10 @@
 consts fold_set :: "[i, i, [i,i]=>i, i] => i"
 
 inductive
-  domains "fold_set(A, B, f,e)" <= "Fin(A)*B"
+  domains "fold_set(A, B, f,e)" \<subseteq> "Fin(A)*B"
   intros
     emptyI: "e\<in>B ==> <0, e>\<in>fold_set(A, B, f,e)"
-    consI:  "[| x\<in>A; x \<notin>C;  <C,y> : fold_set(A, B,f,e); f(x,y):B |]
+    consI:  "[| x\<in>A; x \<notin>C;  <C,y> \<in> fold_set(A, B,f,e); f(x,y):B |]
                 ==>  <cons(x,C), f(x,y)>\<in>fold_set(A, B, f, e)"
   type_intros Fin.intros
   
@@ -29,12 +29,12 @@
 
 (** foldSet **)
 
-inductive_cases empty_fold_setE: "<0, x> : fold_set(A, B, f,e)"
-inductive_cases cons_fold_setE: "<cons(x,C), y> : fold_set(A, B, f,e)"
+inductive_cases empty_fold_setE: "<0, x> \<in> fold_set(A, B, f,e)"
+inductive_cases cons_fold_setE: "<cons(x,C), y> \<in> fold_set(A, B, f,e)"
 
 (* add-hoc lemmas *)                                                
 
-lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) <-> B = C"
+lemma cons_lemma1: "[| x\<notin>C; x\<notin>B |] ==> cons(x,B)=cons(x,C) \<longleftrightarrow> B = C"
 by (auto elim: equalityE)
 
 lemma cons_lemma2: "[| cons(x, B)=cons(y, C); x\<noteq>y; x\<notin>B; y\<notin>C |]  
@@ -44,13 +44,13 @@
 
 (* fold_set monotonicity *)
 lemma fold_set_mono_lemma:
-     "<C, x> : fold_set(A, B, f, e)  
-      ==> ALL D. A<=D --> <C, x> : fold_set(D, B, f, e)"
+     "<C, x> \<in> fold_set(A, B, f, e)  
+      ==> \<forall>D. A<=D \<longrightarrow> <C, x> \<in> fold_set(D, B, f, e)"
 apply (erule fold_set.induct)
 apply (auto intro: fold_set.intros)
 done
 
-lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) <= fold_set(A, B, f, e)"
+lemma fold_set_mono: " C<=A ==> fold_set(C, B, f, e) \<subseteq> fold_set(A, B, f, e)"
 apply clarify
 apply (frule fold_set.dom_subset [THEN subsetD], clarify)
 apply (auto dest: fold_set_mono_lemma)
@@ -64,8 +64,8 @@
 
 (* Proving that fold_set is deterministic *)
 lemma Diff1_fold_set:
-     "[| <C-{x},y> : fold_set(A, B, f,e);  x\<in>C; x\<in>A; f(x, y):B |]  
-      ==> <C, f(x, y)> : fold_set(A, B, f, e)"
+     "[| <C-{x},y> \<in> fold_set(A, B, f,e);  x\<in>C; x\<in>A; f(x, y):B |]  
+      ==> <C, f(x, y)> \<in> fold_set(A, B, f, e)"
 apply (frule fold_set.dom_subset [THEN subsetD])
 apply (erule cons_Diff [THEN subst], rule fold_set.intros, auto)
 done
@@ -79,7 +79,7 @@
 
 
 lemma (in fold_typing) Fin_imp_fold_set:
-     "C\<in>Fin(A) ==> (EX x. <C, x> : fold_set(A, B, f,e))"
+     "C\<in>Fin(A) ==> (\<exists>x. <C, x> \<in> fold_set(A, B, f,e))"
 apply (erule Fin_induct)
 apply (auto dest: fold_set.dom_subset [THEN subsetD] 
             intro: fold_set.intros etype ftype)
@@ -91,9 +91,9 @@
 
 lemma (in fold_typing) fold_set_determ_lemma [rule_format]: 
 "n\<in>nat
- ==> ALL C. |C|<n -->  
-   (ALL x. <C, x> : fold_set(A, B, f,e)--> 
-           (ALL y. <C, y> : fold_set(A, B, f,e) --> y=x))"
+ ==> \<forall>C. |C|<n \<longrightarrow>  
+   (\<forall>x. <C, x> \<in> fold_set(A, B, f,e)\<longrightarrow> 
+           (\<forall>y. <C, y> \<in> fold_set(A, B, f,e) \<longrightarrow> y=x))"
 apply (erule nat_induct)
  apply (auto simp add: le_iff)
 apply (erule fold_set.cases)
@@ -110,7 +110,7 @@
 apply (drule cons_lemma2, safe)
 apply (frule Diff_sing_imp, assumption+) 
 txt{** LEVEL 17*}
-apply (subgoal_tac "|Ca| le |Cb|")
+apply (subgoal_tac "|Ca| \<le> |Cb|")
  prefer 2
  apply (rule succ_le_imp_le)
  apply (simp add: Fin_into_Finite Finite_imp_succ_cardinal_Diff 
@@ -122,7 +122,7 @@
 apply (blast dest!: ftype fold_set.dom_subset [THEN subsetD])
 apply (subgoal_tac "ya = f(xb,xa) ")
  prefer 2 apply (blast del: equalityCE)
-apply (subgoal_tac "<Cb-{x}, xa> : fold_set(A,B,f,e)")
+apply (subgoal_tac "<Cb-{x}, xa> \<in> fold_set(A,B,f,e)")
  prefer 2 apply simp
 apply (subgoal_tac "yb = f (x, xa) ")
  apply (drule_tac [2] C = Cb in Diff1_fold_set, simp_all)
@@ -143,7 +143,7 @@
 (** The fold function **)
 
 lemma (in fold_typing) fold_equality: 
-     "<C,y> : fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
+     "<C,y> \<in> fold_set(A,B,f,e) ==> fold[B](f,e,C) = y"
 apply (unfold fold_def)
 apply (frule fold_set.dom_subset [THEN subsetD], clarify)
 apply (rule the_equality)
@@ -154,15 +154,15 @@
 apply (auto dest: fold_set_lemma intro: ftype etype fcomm)
 done
 
-lemma fold_0 [simp]: "e : B ==> fold[B](f,e,0) = e"
+lemma fold_0 [simp]: "e \<in> B ==> fold[B](f,e,0) = e"
 apply (unfold fold_def)
 apply (blast elim!: empty_fold_setE intro: fold_set.intros)
 done
 
 text{*This result is the right-to-left direction of the subsequent result*}
 lemma (in fold_typing) fold_set_imp_cons: 
-     "[| <C, y> : fold_set(C, B, f, e); C : Fin(A); c : A; c\<notin>C |]
-      ==> <cons(c, C), f(c,y)> : fold_set(cons(c, C), B, f, e)"
+     "[| <C, y> \<in> fold_set(C, B, f, e); C \<in> Fin(A); c \<in> A; c\<notin>C |]
+      ==> <cons(c, C), f(c,y)> \<in> fold_set(cons(c, C), B, f, e)"
 apply (frule FinD [THEN fold_set_mono, THEN subsetD])
  apply assumption
 apply (frule fold_set.dom_subset [of A, THEN subsetD])
@@ -170,9 +170,9 @@
 done
 
 lemma (in fold_typing) fold_cons_lemma [rule_format]: 
-"[| C : Fin(A); c : A; c\<notin>C |]   
-     ==> <cons(c, C), v> : fold_set(cons(c, C), B, f, e) <->   
-         (EX y. <C, y> : fold_set(C, B, f, e) & v = f(c, y))"
+"[| C \<in> Fin(A); c \<in> A; c\<notin>C |]   
+     ==> <cons(c, C), v> \<in> fold_set(cons(c, C), B, f, e) \<longleftrightarrow>   
+         (\<exists>y. <C, y> \<in> fold_set(C, B, f, e) & v = f(c, y))"
 apply auto
  prefer 2 apply (blast intro: fold_set_imp_cons) 
  apply (frule_tac Fin.consI [of c, THEN FinD, THEN fold_set_mono, THEN subsetD], assumption+)
@@ -220,7 +220,7 @@
 lemma (in fold_typing) fold_nest_Un_Int: 
      "[| C\<in>Fin(A); D\<in>Fin(A) |]
       ==> fold[B](f, fold[B](f, e, D), C) =
-          fold[B](f, fold[B](f, e, (C Int D)), C Un D)"
+          fold[B](f, fold[B](f, e, (C \<inter> D)), C \<union> D)"
 apply (erule Fin_induct, auto)
 apply (simp add: Un_cons Int_cons_left fold_type fold_commute
                  fold_typing.fold_cons [of A _ _ f] 
@@ -228,8 +228,8 @@
 done
 
 lemma (in fold_typing) fold_nest_Un_disjoint:
-     "[| C\<in>Fin(A); D\<in>Fin(A); C Int D = 0 |]  
-      ==> fold[B](f,e,C Un D) =  fold[B](f, fold[B](f,e,D), C)"
+     "[| C\<in>Fin(A); D\<in>Fin(A); C \<inter> D = 0 |]  
+      ==> fold[B](f,e,C \<union> D) =  fold[B](f, fold[B](f,e,D), C)"
 by (simp add: fold_nest_Un_Int)
 
 lemma Finite_cons_lemma: "Finite(C) ==> C\<in>Fin(cons(c, C))"
@@ -245,7 +245,7 @@
 lemma setsum_cons [simp]: 
      "Finite(C) ==> 
       setsum(g, cons(c,C)) = 
-        (if c : C then setsum(g,C) else g(c) $+ setsum(g,C))"
+        (if c \<in> C then setsum(g,C) else g(c) $+ setsum(g,C))"
 apply (auto simp add: setsum_def Finite_cons cons_absorb)
 apply (rule_tac A = "cons (c, C)" in fold_typing.fold_cons)
 apply (auto intro: fold_typing.intro Finite_cons_lemma)
@@ -260,7 +260,7 @@
 (*The reversed orientation looks more natural, but LOOPS as a simprule!*)
 lemma setsum_Un_Int:
      "[| Finite(C); Finite(D) |]  
-      ==> setsum(g, C Un D) $+ setsum(g, C Int D)  
+      ==> setsum(g, C \<union> D) $+ setsum(g, C \<inter> D)  
         = setsum(g, C) $+ setsum(g, D)"
 apply (erule Finite_induct)
 apply (simp_all add: Int_cons_right cons_absorb Un_cons Int_commute Finite_Un
@@ -274,27 +274,27 @@
 done
 
 lemma setsum_Un_disjoint:
-     "[| Finite(C); Finite(D); C Int D = 0 |]  
-      ==> setsum(g, C Un D) = setsum(g, C) $+ setsum(g,D)"
+     "[| Finite(C); Finite(D); C \<inter> D = 0 |]  
+      ==> setsum(g, C \<union> D) = setsum(g, C) $+ setsum(g,D)"
 apply (subst setsum_Un_Int [symmetric])
-apply (subgoal_tac [3] "Finite (C Un D) ")
+apply (subgoal_tac [3] "Finite (C \<union> D) ")
 apply (auto intro: Finite_Un)
 done
 
 lemma Finite_RepFun [rule_format (no_asm)]:
-     "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) --> Finite(RepFun(I, C))"
+     "Finite(I) ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow> Finite(RepFun(I, C))"
 apply (erule Finite_induct, auto)
 done
 
 lemma setsum_UN_disjoint [rule_format (no_asm)]:
      "Finite(I)  
-      ==> (\<forall>i\<in>I. Finite(C(i))) -->  
-          (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j --> C(i) Int C(j) = 0) -->  
+      ==> (\<forall>i\<in>I. Finite(C(i))) \<longrightarrow>  
+          (\<forall>i\<in>I. \<forall>j\<in>I. i\<noteq>j \<longrightarrow> C(i) \<inter> C(j) = 0) \<longrightarrow>  
           setsum(f, \<Union>i\<in>I. C(i)) = setsum (%i. setsum(f, C(i)), I)"
 apply (erule Finite_induct, auto)
 apply (subgoal_tac "\<forall>i\<in>B. x \<noteq> i")
  prefer 2 apply blast
-apply (subgoal_tac "C (x) Int (\<Union>i\<in>B. C (i)) = 0")
+apply (subgoal_tac "C (x) \<inter> (\<Union>i\<in>B. C (i)) = 0")
  prefer 2 apply blast
 apply (subgoal_tac "Finite (\<Union>i\<in>B. C (i)) & Finite (C (x)) & Finite (B) ")
 apply (simp (no_asm_simp) add: setsum_Un_disjoint)
@@ -332,21 +332,21 @@
 
 lemma setsum_Un:
      "[| Finite(A); Finite(B) |]  
-      ==> setsum(f, A Un B) =  
-          setsum(f, A) $+ setsum(f, B) $- setsum(f, A Int B)"
+      ==> setsum(f, A \<union> B) =  
+          setsum(f, A) $+ setsum(f, B) $- setsum(f, A \<inter> B)"
 apply (subst setsum_Un_Int [symmetric], auto)
 done
 
 
 lemma setsum_zneg_or_0 [rule_format (no_asm)]:
-     "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) --> setsum(g, A) $<= #0"
+     "Finite(A) ==> (\<forall>x\<in>A. g(x) $<= #0) \<longrightarrow> setsum(g, A) $<= #0"
 apply (erule Finite_induct)
 apply (auto intro: zneg_or_0_add_zneg_or_0_imp_zneg_or_0)
 done
 
 lemma setsum_succD_lemma [rule_format]:
      "Finite(A)  
-      ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) --> (\<exists>a\<in>A. #0 $< f(a))"
+      ==> \<forall>n\<in>nat. setsum(f,A) = $# succ(n) \<longrightarrow> (\<exists>a\<in>A. #0 $< f(a))"
 apply (erule Finite_induct)
 apply (auto simp del: int_of_0 int_of_succ simp add: not_zless_iff_zle int_of_0 [symmetric])
 apply (subgoal_tac "setsum (f, B) $<= #0")
@@ -368,7 +368,7 @@
 done
 
 lemma g_zpos_imp_setsum_zpos [rule_format]:
-     "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) --> #0 $<= setsum(g, A)"
+     "Finite(A) ==> (\<forall>x\<in>A. #0 $<= g(x)) \<longrightarrow> #0 $<= setsum(g, A)"
 apply (erule Finite_induct)
 apply (simp (no_asm))
 apply (auto intro: zpos_add_zpos_imp_zpos)
@@ -382,13 +382,13 @@
 
 lemma g_zspos_imp_setsum_zspos [rule_format]:
      "Finite(A)  
-      ==> (\<forall>x\<in>A. #0 $< g(x)) --> A \<noteq> 0 --> (#0 $< setsum(g, A))"
+      ==> (\<forall>x\<in>A. #0 $< g(x)) \<longrightarrow> A \<noteq> 0 \<longrightarrow> (#0 $< setsum(g, A))"
 apply (erule Finite_induct)
 apply (auto intro: zspos_add_zspos_imp_zspos)
 done
 
 lemma setsum_Diff [rule_format]:
-     "Finite(A) ==> \<forall>a. M(a) = #0 --> setsum(M, A) = setsum(M, A-{a})"
+     "Finite(A) ==> \<forall>a. M(a) = #0 \<longrightarrow> setsum(M, A) = setsum(M, A-{a})"
 apply (erule Finite_induct) 
 apply (simp_all add: Diff_cons_eq Finite_Diff) 
 done
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/ListN.thy
--- a/src/ZF/Induct/ListN.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/ListN.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -24,7 +24,7 @@
 lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
   by (induct set: list) (simp_all add: listn.intros)
 
-lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n"
+lemma listn_iff: "<n,l> \<in> listn(A) \<longleftrightarrow> l \<in> list(A) & length(l)=n"
   apply (rule iffI)
    apply (erule listn.induct)
     apply auto
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Multiset.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -34,8 +34,8 @@
 
 definition
   munion    :: "[i, i] => i" (infixl "+#" 65)  where
-  "M +# N == \<lambda>x \<in> mset_of(M) Un mset_of(N).
-     if x \<in> mset_of(M) Int mset_of(N) then  (M`x) #+ (N`x)
+  "M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N).
+     if x \<in> mset_of(M) \<inter> mset_of(N) then  (M`x) #+ (N`x)
      else (if x \<in> mset_of(M) then M`x else N`x)"
 
 definition
@@ -74,7 +74,7 @@
   "a :# M == a \<in> mset_of(M)"
 
 syntax
-  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
+  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
 syntax (xsymbols)
   "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
 translations
@@ -144,7 +144,7 @@
 
 text{* A useful simplification rule *}
 lemma multiset_fun_iff:
-     "(f \<in> A -> nat-{0}) <-> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)"
+     "(f \<in> A -> nat-{0}) \<longleftrightarrow> f \<in> A->nat&(\<forall>a \<in> A. f`a \<in> nat & 0 < f`a)"
 apply safe
 apply (rule_tac [4] B1 = "range (f) " in Pi_mono [THEN subsetD])
 apply (auto intro!: Ord_0_lt
@@ -170,10 +170,10 @@
 apply (blast intro: Fin_into_Finite)
 done
 
-lemma Mult_iff_multiset: "M \<in> Mult(A) <-> multiset(M) & mset_of(M)\<subseteq>A"
+lemma Mult_iff_multiset: "M \<in> Mult(A) \<longleftrightarrow> multiset(M) & mset_of(M)\<subseteq>A"
 by (blast dest: Mult_into_multiset intro: multiset_into_Mult)
 
-lemma multiset_iff_Mult_mset_of: "multiset(M) <-> M \<in> Mult(mset_of(M))"
+lemma multiset_iff_Mult_mset_of: "multiset(M) \<longleftrightarrow> M \<in> Mult(mset_of(M))"
 by (auto simp add: Mult_iff_multiset)
 
 
@@ -193,13 +193,13 @@
 lemma mset_of_0 [iff]: "mset_of(0) = 0"
 by (simp add: mset_of_def)
 
-lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 <-> M=0"
+lemma mset_is_0_iff: "multiset(M) ==> mset_of(M)=0 \<longleftrightarrow> M=0"
 by (auto simp add: multiset_def mset_of_def)
 
 lemma mset_of_single [iff]: "mset_of({#a#}) = {a}"
 by (simp add: msingle_def mset_of_def)
 
-lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) Un mset_of(N)"
+lemma mset_of_union [iff]: "mset_of(M +# N) = mset_of(M) \<union> mset_of(N)"
 by (simp add: mset_of_def munion_def)
 
 lemma mset_of_diff [simp]: "mset_of(M)\<subseteq>A ==> mset_of(M -# N) \<subseteq> A"
@@ -210,7 +210,7 @@
 lemma msingle_not_0 [iff]: "{#a#} \<noteq> 0 & 0 \<noteq> {#a#}"
 by (simp add: msingle_def)
 
-lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) <->  (a = b)"
+lemma msingle_eq_iff [iff]: "({#a#} = {#b#}) \<longleftrightarrow>  (a = b)"
 by (simp add: msingle_def)
 
 lemma msingle_multiset [iff,TC]: "multiset({#a#})"
@@ -248,7 +248,7 @@
 
 lemma munion_multiset [simp]: "[| multiset(M); multiset(N) |] ==> multiset(M +# N)"
 apply (unfold multiset_def munion_def mset_of_def, auto)
-apply (rule_tac x = "A Un Aa" in exI)
+apply (rule_tac x = "A \<union> Aa" in exI)
 apply (auto intro!: lam_type intro: Finite_Un simp add: multiset_fun_iff zero_less_add)
 done
 
@@ -298,7 +298,7 @@
 prefer 2 apply (force intro!: lam_type)
 apply (subgoal_tac [2] "{x \<in> A \<union> {a} . x \<noteq> a \<and> x \<in> A} = A")
 apply (rule fun_extension, auto)
-apply (drule_tac x = "A Un {a}" in spec)
+apply (drule_tac x = "A \<union> {a}" in spec)
 apply (simp add: Finite_Un)
 apply (force intro!: lam_type)
 done
@@ -361,7 +361,7 @@
 apply (blast dest!: fun_is_rel)
 done
 
-lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 <-> M=0"
+lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 \<longleftrightarrow> M=0"
 apply (simp add: msize_def, auto)
 apply (rule_tac P = "setsum (?u,?v) \<noteq> #0" in swap)
 apply blast
@@ -378,11 +378,11 @@
 done
 
 lemma setsum_mcount_Int:
-     "Finite(A) ==> setsum(%a. $# mcount(N, a), A Int mset_of(N))
+     "Finite(A) ==> setsum(%a. $# mcount(N, a), A \<inter> mset_of(N))
                   = setsum(%a. $# mcount(N, a), A)"
 apply (induct rule: Finite_induct)
  apply auto
-apply (subgoal_tac "Finite (B Int mset_of (N))")
+apply (subgoal_tac "Finite (B \<inter> mset_of (N))")
 prefer 2 apply (blast intro: subset_Finite)
 apply (auto simp add: mcount_def Int_cons_left)
 done
@@ -412,7 +412,7 @@
 done
 
 lemma multiset_equality:
-  "[| multiset(M); multiset(N) |]==> M=N<->(\<forall>a. mcount(M, a)=mcount(N, a))"
+  "[| multiset(M); multiset(N) |]==> M=N\<longleftrightarrow>(\<forall>a. mcount(M, a)=mcount(N, a))"
 apply auto
 apply (subgoal_tac "mset_of (M) = mset_of (N) ")
 prefer 2 apply (blast intro: equality_lemma)
@@ -426,28 +426,28 @@
 
 (** More algebraic properties of multisets **)
 
-lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) <-> (M=0 & N=0)"
+lemma munion_eq_0_iff [simp]: "[|multiset(M); multiset(N)|]==>(M +# N =0) \<longleftrightarrow> (M=0 & N=0)"
 by (auto simp add: multiset_equality)
 
-lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) <-> (M=0 & N=0)"
+lemma empty_eq_munion_iff [simp]: "[|multiset(M); multiset(N)|]==>(0=M +# N) \<longleftrightarrow> (M=0 & N=0)"
 apply (rule iffI, drule sym)
 apply (simp_all add: multiset_equality)
 done
 
 lemma munion_right_cancel [simp]:
-     "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)<->(M=N)"
+     "[| multiset(M); multiset(N); multiset(K) |]==>(M +# K = N +# K)\<longleftrightarrow>(M=N)"
 by (auto simp add: multiset_equality)
 
 lemma munion_left_cancel [simp]:
-  "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) <-> (M = N)"
+  "[|multiset(K); multiset(M); multiset(N)|] ==>(K +# M = K +# N) \<longleftrightarrow> (M = N)"
 by (auto simp add: multiset_equality)
 
-lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) <-> (m=1 & n=0) | (m=0 & n=1)"
+lemma nat_add_eq_1_cases: "[| m \<in> nat; n \<in> nat |] ==> (m #+ n = 1) \<longleftrightarrow> (m=1 & n=0) | (m=0 & n=1)"
 by (induct_tac n) auto
 
 lemma munion_is_single:
      "[|multiset(M); multiset(N)|] 
-      ==> (M +# N = {#a#}) <->  (M={#a#} & N=0) | (M = 0 & N = {#a#})"
+      ==> (M +# N = {#a#}) \<longleftrightarrow>  (M={#a#} & N=0) | (M = 0 & N = {#a#})"
 apply (simp (no_asm_simp) add: multiset_equality)
 apply safe
 apply simp_all
@@ -467,8 +467,8 @@
 done
 
 lemma msingle_is_union: "[| multiset(M); multiset(N) |]
-  ==> ({#a#} = M +# N) <-> ({#a#} = M  & N=0 | M = 0 & {#a#} = N)"
-apply (subgoal_tac " ({#a#} = M +# N) <-> (M +# N = {#a#}) ")
+  ==> ({#a#} = M +# N) \<longleftrightarrow> ({#a#} = M  & N=0 | M = 0 & {#a#} = N)"
+apply (subgoal_tac " ({#a#} = M +# N) \<longleftrightarrow> (M +# N = {#a#}) ")
 apply (simp (no_asm_simp) add: munion_is_single)
 apply blast
 apply (blast dest: sym)
@@ -478,7 +478,7 @@
 
 lemma setsum_decr:
 "Finite(A)
-  ==>  (\<forall>M. multiset(M) -->
+  ==>  (\<forall>M. multiset(M) \<longrightarrow>
   (\<forall>a \<in> mset_of(M). setsum(%z. $# mcount(M(a:=M`a #- 1), z), A) =
   (if a \<in> A then setsum(%z. $# mcount(M, z), A) $- #1
            else setsum(%z. $# mcount(M, z), A))))"
@@ -494,7 +494,7 @@
 
 lemma setsum_decr2:
      "Finite(A)
-      ==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M).
+      ==> \<forall>M. multiset(M) \<longrightarrow> (\<forall>a \<in> mset_of(M).
            setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) =
            (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
             else setsum(%x. $# mcount(M, x), A)))"
@@ -514,11 +514,11 @@
 apply (simp add: mcount_def mset_of_def)
 done
 
-lemma nat_le_1_cases: "n \<in> nat ==> n le 1 <-> (n=0 | n=1)"
+lemma nat_le_1_cases: "n \<in> nat ==> n \<le> 1 \<longleftrightarrow> (n=0 | n=1)"
 by (auto elim: natE)
 
 lemma succ_pred_eq_self: "[| 0<n; n \<in> nat |] ==> succ(n #- 1) = n"
-apply (subgoal_tac "1 le n")
+apply (subgoal_tac "1 \<le> n")
 apply (drule add_diff_inverse2, auto)
 done
 
@@ -536,8 +536,8 @@
       and prem2: "!!M b. [| multiset(M); b \<in> mset_of(M); P(M) |] ==> P(M(b:= M`b #+ 1))"
   shows
   "[| n \<in> nat; P(0) |]
-     ==> (\<forall>M. multiset(M)-->
-  (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) --> P(M))"
+     ==> (\<forall>M. multiset(M)\<longrightarrow>
+  (setsum(%x. $# mcount(M, x), {x \<in> mset_of(M). 0 < M`x}) = $# n) \<longrightarrow> P(M))"
 apply (erule nat_induct, clarify)
 apply (frule msize_eq_0_iff)
 apply (auto simp add: mset_of_def multiset_def multiset_fun_iff msize_def)
@@ -562,9 +562,9 @@
 apply (drule mp, drule_tac [2] mp, simp_all)
 apply (rule_tac x = A in exI)
 apply (auto intro: update_type)
-apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a-->0<M`x}) ")
+apply (subgoal_tac "Finite ({x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}) ")
 prefer 2 apply (blast intro: Collect_subset [THEN subset_Finite] Finite_cons)
-apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a-->0<M`x}" in setsum_decr)
+apply (drule_tac A = "{x \<in> cons (a, A) . x\<noteq>a\<longrightarrow>0<M`x}" in setsum_decr)
 apply (drule_tac x = M in spec)
 apply (subgoal_tac "multiset (M) ")
  prefer 2
@@ -631,7 +631,7 @@
 apply (simp add: multiset_def)
 apply (auto simp add: munion_def multiset_fun_iff msingle_def)
 apply (unfold mset_of_def, simp)
-apply (subgoal_tac "A Un {a} = A")
+apply (subgoal_tac "A \<union> {a} = A")
 apply (rule fun_extension)
 apply (auto dest: domain_type intro: lam_type update_type)
 done
@@ -665,7 +665,7 @@
 by (auto simp add: mset_of_def MCollect_def multiset_def funrestrict_def)
 
 lemma MCollect_mem_iff [iff]:
-     "x \<in> mset_of({#x \<in> M. P(x)#}) <->  x \<in> mset_of(M) & P(x)"
+     "x \<in> mset_of({#x \<in> M. P(x)#}) \<longleftrightarrow>  x \<in> mset_of(M) & P(x)"
 by (simp add: MCollect_def mset_of_def)
 
 lemma mcount_MCollect [simp]:
@@ -682,7 +682,7 @@
 (* and more algebraic laws on multisets *)
 
 lemma munion_eq_conv_diff: "[| multiset(M); multiset(N) |]
-  ==>  (M +# {#a#} = N +# {#b#}) <->  (M = N & a = b |
+  ==>  (M +# {#a#} = N +# {#b#}) \<longleftrightarrow>  (M = N & a = b |
        M = N -# {#a#} +# {#b#} & N = M -# {#b#} +# {#a#})"
 apply (simp del: mcount_single add: multiset_equality)
 apply (rule iffI, erule_tac [2] disjE, erule_tac [3] conjE)
@@ -697,7 +697,7 @@
 
 lemma melem_diff_single:
 "multiset(M) ==>
-  k \<in> mset_of(M -# {#a#}) <-> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))"
+  k \<in> mset_of(M -# {#a#}) \<longleftrightarrow> (k=a & 1 < mcount(M,a)) | (k\<noteq> a & k \<in> mset_of(M))"
 apply (simp add: multiset_def)
 apply (simp add: normalize_def mset_of_def msingle_def mdiff_def mcount_def)
 apply (auto dest: domain_type intro: zero_less_diff [THEN iffD1]
@@ -709,7 +709,7 @@
 
 lemma munion_eq_conv_exist:
 "[| M \<in> Mult(A); N \<in> Mult(A) |]
-  ==> (M +# {#a#} = N +# {#b#}) <->
+  ==> (M +# {#a#} = N +# {#b#}) \<longleftrightarrow>
       (M=N & a=b | (\<exists>K \<in> Mult(A). M= K +# {#b#} & N=K +# {#a#}))"
 by (auto simp add: Mult_iff_multiset melem_diff_single munion_eq_conv_diff)
 
@@ -728,7 +728,7 @@
 by (auto simp add: multirel1_def)
 
 lemma multirel1_iff:
-" <N, M> \<in> multirel1(A, r) <->
+" <N, M> \<in> multirel1(A, r) \<longleftrightarrow>
   (\<exists>a. a \<in> A &
   (\<exists>M0. M0 \<in> Mult(A) & (\<exists>K. K \<in> Mult(A) &
    M=M0 +# {#a#} & N=M0 +# K & (\<forall>b \<in> mset_of(K). <b,a> \<in> r))))"
@@ -789,10 +789,10 @@
 lemma acc_0: "acc(0)=0"
 by (auto intro!: equalityI dest: acc.dom_subset [THEN subsetD])
 
-lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r -->
+lemma lemma1: "[| \<forall>b \<in> A. <b,a> \<in> r \<longrightarrow>
     (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#}:acc(multirel1(A, r)));
     M0 \<in> acc(multirel1(A, r)); a \<in> A;
-    \<forall>M. <M,M0> \<in> multirel1(A, r) --> M +# {#a#} \<in> acc(multirel1(A, r)) |]
+    \<forall>M. <M,M0> \<in> multirel1(A, r) \<longrightarrow> M +# {#a#} \<in> acc(multirel1(A, r)) |]
   ==> M0 +# {#a#} \<in> acc(multirel1(A, r))"
 apply (subgoal_tac "M0 \<in> Mult(A) ")
  prefer 2
@@ -822,7 +822,7 @@
 done
 
 lemma lemma2: "[| \<forall>b \<in> A. <b,a> \<in> r
-   --> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));
+   \<longrightarrow> (\<forall>M \<in> acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r)));
         M \<in> acc(multirel1(A, r)); a \<in> A|] ==> M +# {#a#} \<in> acc(multirel1(A, r))"
 apply (erule acc_induct)
 apply (blast intro: lemma1)
@@ -834,8 +834,8 @@
 apply (blast intro: lemma2)
 done
 
-lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A -->
-   wf[A](r) --> M \<in> field(multirel1(A, r)) --> M \<in> acc(multirel1(A, r))"
+lemma lemma4: "multiset(M) ==> mset_of(M)\<subseteq>A \<longrightarrow>
+   wf[A](r) \<longrightarrow> M \<in> field(multirel1(A, r)) \<longrightarrow> M \<in> acc(multirel1(A, r))"
 apply (erule multiset_induct)
 (* proving the base case *)
 apply clarify
@@ -899,7 +899,7 @@
 
 (* Equivalence of multirel with the usual (closure-free) def *)
 
-lemma add_diff_eq: "k \<in> nat ==> 0 < k --> n #+ k #- 1 = n #+ (k #- 1)"
+lemma add_diff_eq: "k \<in> nat ==> 0 < k \<longrightarrow> n #+ k #- 1 = n #+ (k #- 1)"
 by (erule nat_induct, auto)
 
 lemma mdiff_union_single_conv: "[|a \<in> mset_of(J); multiset(I); multiset(J) |]
@@ -910,14 +910,14 @@
 apply (auto dest: domain_type simp add: add_diff_eq)
 done
 
-lemma diff_add_commute: "[| n le m;  m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n"
+lemma diff_add_commute: "[| n \<le> m;  m \<in> nat; n \<in> nat; k \<in> nat |] ==> m #- n #+ k = m #+ k #- n"
 by (auto simp add: le_iff less_iff_succ_add)
 
 (* One direction *)
 
 lemma multirel_implies_one_step:
 "<M,N> \<in> multirel(A, r) ==>
-     trans[A](r) -->
+     trans[A](r) \<longrightarrow>
      (\<exists>I J K.
          I \<in> Mult(A) & J \<in> Mult(A) &  K \<in> Mult(A) &
          N = I +# J & M = I +# K & J \<noteq> 0 &
@@ -986,7 +986,7 @@
    (\<forall>I J K.
     I \<in> Mult(A) & J \<in> Mult(A) & K \<in> Mult(A) &
    (msize(J) = $# n & J \<noteq>0 &  (\<forall>k \<in> mset_of(K).  \<exists>j \<in> mset_of(J). <k, j> \<in> r))
-    --> <I +# K, I +# J> \<in> multirel(A, r))"
+    \<longrightarrow> <I +# K, I +# J> \<in> multirel(A, r))"
 apply (simp add: Mult_iff_multiset)
 apply (erule nat_induct, clarify)
 apply (drule_tac M = J in msize_eq_0_iff, auto)
@@ -1039,7 +1039,7 @@
 (*irreflexivity*)
 
 lemma multirel_irrefl_lemma:
-     "Finite(A) ==> part_ord(A, r) --> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) -->A=0"
+     "Finite(A) ==> part_ord(A, r) \<longrightarrow> (\<forall>x \<in> A. \<exists>y \<in> A. <x,y> \<in> r) \<longrightarrow>A=0"
 apply (erule Finite_induct)
 apply (auto dest: subset_consI [THEN [2] part_ord_subset])
 apply (auto simp add: part_ord_def irrefl_def)
@@ -1152,7 +1152,7 @@
 
 lemma munion_omultiset [simp]: "[| omultiset(M); omultiset(N) |] ==> omultiset(M +# N)"
 apply (simp add: omultiset_def, clarify)
-apply (rule_tac x = "i Un ia" in exI)
+apply (rule_tac x = "i \<union> ia" in exI)
 apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
 apply (blast intro: field_Memrel_mono)
 done
@@ -1173,7 +1173,7 @@
 apply (drule_tac i = x in ltI [THEN lt_irrefl], auto)
 done
 
-lemma trans_iff_trans_on: "trans(r) <-> trans[field(r)](r)"
+lemma trans_iff_trans_on: "trans(r) \<longleftrightarrow> trans[field(r)](r)"
 by (simp add: trans_on_def trans_def, auto)
 
 lemma part_ord_Memrel: "Ord(i) ==>part_ord(field(Memrel(i)), Memrel(i))"
@@ -1204,7 +1204,7 @@
 (*transitivity*)
 lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N"
 apply (simp add: mless_def, clarify)
-apply (rule_tac x = "i Un ia" in exI)
+apply (rule_tac x = "i \<union> ia" in exI)
 apply (blast dest: multirel_Memrel_mono [OF Un_upper1 Un_upper1, THEN subsetD]
                    multirel_Memrel_mono [OF Un_upper2 Un_upper2, THEN subsetD]
         intro: multirel_trans Ord_Un)
@@ -1236,14 +1236,14 @@
 apply (blast intro: mless_trans)
 done
 
-lemma mless_le_iff: "M <# N <-> (M <#= N & M \<noteq> N)"
+lemma mless_le_iff: "M <# N \<longleftrightarrow> (M <#= N & M \<noteq> N)"
 by (simp add: mle_def, auto)
 
 (** Monotonicity of mless **)
 
 lemma munion_less_mono2: "[| M <# N; omultiset(K) |] ==> K +# M <# K +# N"
 apply (simp add: mless_def omultiset_def, clarify)
-apply (rule_tac x = "i Un ia" in exI)
+apply (rule_tac x = "i \<union> ia" in exI)
 apply (simp add: Mult_iff_multiset Ord_Un Un_subset_iff)
 apply (rule munion_multirel_mono2)
  apply (blast intro: multirel_Memrel_mono [THEN subsetD])
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/Mutil.thy
--- a/src/ZF/Induct/Mutil.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/Mutil.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -24,10 +24,10 @@
   type_intros empty_subsetI cons_subsetI PowI SigmaI nat_succI
 
 inductive
-  domains "tiling(A)" \<subseteq> "Pow(Union(A))"
+  domains "tiling(A)" \<subseteq> "Pow(\<Union>(A))"
   intros
     empty: "0 \<in> tiling(A)"
-    Un: "[| a \<in> A;  t \<in> tiling(A);  a Int t = 0 |] ==> a Un t \<in> tiling(A)"
+    Un: "[| a \<in> A;  t \<in> tiling(A);  a \<inter> t = 0 |] ==> a \<union> t \<in> tiling(A)"
   type_intros empty_subsetI Union_upper Un_least PowI
   type_elims PowD [elim_format]
 
@@ -38,7 +38,7 @@
 
 subsection {* Basic properties of evnodd *}
 
-lemma evnodd_iff: "<i,j>: evnodd(A,b) <-> <i,j>: A & (i#+j) mod 2 = b"
+lemma evnodd_iff: "<i,j>: evnodd(A,b) \<longleftrightarrow> <i,j>: A & (i#+j) mod 2 = b"
   by (unfold evnodd_def) blast
 
 lemma evnodd_subset: "evnodd(A, b) \<subseteq> A"
@@ -47,7 +47,7 @@
 lemma Finite_evnodd: "Finite(X) ==> Finite(evnodd(X,b))"
   by (rule lepoll_Finite, rule subset_imp_lepoll, rule evnodd_subset)
 
-lemma evnodd_Un: "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)"
+lemma evnodd_Un: "evnodd(A \<union> B, b) = evnodd(A,b) \<union> evnodd(B,b)"
   by (simp add: evnodd_def Collect_Un)
 
 lemma evnodd_Diff: "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"
@@ -83,7 +83,7 @@
 text {* The union of two disjoint tilings is a tiling *}
 
 lemma tiling_UnI:
-    "t \<in> tiling(A) ==> u \<in> tiling(A) ==> t Int u = 0 ==> t Un u \<in> tiling(A)"
+    "t \<in> tiling(A) ==> u \<in> tiling(A) ==> t \<inter> u = 0 ==> t \<union> u \<in> tiling(A)"
   apply (induct set: tiling)
    apply (simp add: tiling.intros)
   apply (simp add: Un_assoc subset_empty_iff [THEN iff_sym])
@@ -108,7 +108,7 @@
     apply simp
    apply assumption
   apply safe
-  apply (subgoal_tac "\<forall>p b. p \<in> evnodd (a,b) --> p\<notin>evnodd (t,b)")
+  apply (subgoal_tac "\<forall>p b. p \<in> evnodd (a,b) \<longrightarrow> p\<notin>evnodd (t,b)")
    apply (simp add: evnodd_Un Un_cons tiling_domino_Finite
      evnodd_subset [THEN subset_Finite] Finite_imp_cardinal_cons)
   apply (blast dest!: evnodd_subset [THEN subsetD] elim: equalityE)
@@ -123,7 +123,7 @@
     prefer 2 apply assumption
    apply (rename_tac n')
    apply (subgoal_tac (*seems the easiest way of turning one to the other*)
-     "{i}*{succ (n'#+n') } Un {i}*{n'#+n'} =
+     "{i}*{succ (n'#+n') } \<union> {i}*{n'#+n'} =
        {<i,n'#+n'>, <i,succ (n'#+n') >}")
     prefer 2 apply blast
   apply (simp add: domino.horiz)
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Induct/PropLog.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -68,13 +68,13 @@
   "is_true(p,t) == is_true_fun(p,t) = 1"
   -- {* this definition is required since predicates can't be recursive *}
 
-lemma is_true_Fls [simp]: "is_true(Fls,t) <-> False"
+lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False"
   by (simp add: is_true_def)
 
-lemma is_true_Var [simp]: "is_true(#v,t) <-> v \<in> t"
+lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t"
   by (simp add: is_true_def)
 
-lemma is_true_Imp [simp]: "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"
+lemma is_true_Imp [simp]: "is_true(p=>q,t) \<longleftrightarrow> (is_true(p,t)\<longrightarrow>is_true(q,t))"
   by (simp add: is_true_def)
 
 
@@ -87,7 +87,7 @@
 
 definition
   logcon :: "[i,i] => o"    (infixl "|=" 50)  where
-  "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) --> is_true(p,t)"
+  "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)"
 
 
 text {*
@@ -335,7 +335,7 @@
   apply (blast intro: propn_Is)
   done
 
-theorem thms_iff: "H \<in> Fin(propn) ==> H |- p <-> H |= p \<and> p \<in> propn"
+theorem thms_iff: "H \<in> Fin(propn) ==> H |- p \<longleftrightarrow> H |= p \<and> p \<in> propn"
   by (blast intro: soundness completeness thms_in_pl)
 
 end
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/CoUnit.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -27,7 +27,7 @@
 inductive_cases ConE: "Con(x) \<in> counit"
   -- {* USELESS because folding on @{term "Con(xa) == xa"} fails. *}
 
-lemma Con_iff: "Con(x) = Con(y) <-> x = y"
+lemma Con_iff: "Con(x) = Con(y) \<longleftrightarrow> x = y"
   -- {* Proving freeness results. *}
   by (auto elim!: counit.free_elims)
 
@@ -55,7 +55,7 @@
 
 inductive_cases Con2E: "Con2(x, y) \<in> counit2"
 
-lemma Con2_iff: "Con2(x, y) = Con2(x', y') <-> x = x' & y = y'"
+lemma Con2_iff: "Con2(x, y) = Con2(x', y') \<longleftrightarrow> x = x' & y = y'"
   -- {* Proving freeness results. *}
   by (fast elim!: counit2.free_elims)
 
@@ -73,7 +73,7 @@
   done
 
 lemma counit2_Int_Vset_subset [rule_format]:
-  "Ord(i) ==> \<forall>x y. x \<in> counit2 --> y \<in> counit2 --> x Int Vset(i) \<subseteq> y"
+  "Ord(i) ==> \<forall>x y. x \<in> counit2 \<longrightarrow> y \<in> counit2 \<longrightarrow> x \<inter> Vset(i) \<subseteq> y"
   -- {* Lemma for proving finality. *}
   apply (erule trans_induct)
   apply (tactic "safe_tac (put_claset subset_cs @{context})")
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Commutation.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -10,7 +10,7 @@
 definition
   square  :: "[i, i, i, i] => o" where
   "square(r,s,t,u) ==
-    (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
+    (\<forall>a b. <a,b> \<in> r \<longrightarrow> (\<forall>c. <a, c> \<in> s \<longrightarrow> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
 
 definition
   commute :: "[i, i] => o" where
@@ -26,7 +26,7 @@
 
 definition
   Church_Rosser :: "i => o" where
-  "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r Un converse(r))^* -->
+  "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r \<union> converse(r))^* \<longrightarrow>
                         (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
 
 definition
@@ -79,11 +79,11 @@
 apply (simp_all add: rtrancl_field)
 done
 
-lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"
+lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r \<union> s, t)"
   unfolding commute_def square_def by blast
 
 lemma diamond_Un:
-     "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)"
+     "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r \<union> s)"
   unfolding diamond_def by (blast intro: commute_Un commute_sym)
 
 lemma diamond_confluent:
@@ -94,7 +94,7 @@
 
 lemma confluent_Un:
  "[| confluent(r); confluent(s); commute(r^*, s^*);
-     relation(r); relation(s) |] ==> confluent(r Un s)"
+     relation(r); relation(s) |] ==> confluent(r \<union> s)"
 apply (unfold confluent_def)
 apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
 apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
@@ -136,7 +136,7 @@
 done
 
 
-lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)"
+lemma Church_Rosser: "Church_Rosser(r) \<longleftrightarrow> confluent(r)"
   by (blast intro: Church_Rosser1 Church_Rosser2)
 
 end
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Group.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -105,7 +105,7 @@
 proof -
   have l_cancel [simp]:
     "\<And>x y z. \<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk> \<Longrightarrow>
-    (x \<cdot> y = x \<cdot> z) <-> (y = z)"
+    (x \<cdot> y = x \<cdot> z) \<longleftrightarrow> (y = z)"
   proof
     fix x y z
     assume G: "x \<in> carrier(G)"  "y \<in> carrier(G)"  "z \<in> carrier(G)"
@@ -178,7 +178,7 @@
 
 lemma (in group) l_cancel [simp]:
   assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
-  shows "(x \<cdot> y = x \<cdot> z) <-> (y = z)"
+  shows "(x \<cdot> y = x \<cdot> z) \<longleftrightarrow> (y = z)"
 proof
   assume eq: "x \<cdot> y = x \<cdot> z"
   hence  "(inv x \<cdot> x) \<cdot> y = (inv x \<cdot> x) \<cdot> z"
@@ -191,7 +191,7 @@
 
 lemma (in group) r_cancel [simp]:
   assumes "x \<in> carrier(G)" "y \<in> carrier(G)" "z \<in> carrier(G)"
-  shows "(y \<cdot> x = z \<cdot> x) <-> (y = z)"
+  shows "(y \<cdot> x = z \<cdot> x) \<longleftrightarrow> (y = z)"
 proof
   assume eq: "y \<cdot> x = z \<cdot> x"
   then have "y \<cdot> (x \<cdot> inv x) = z \<cdot> (x \<cdot> inv x)"
@@ -679,9 +679,9 @@
 
 text{*Alternative characterization of normal subgroups*}
 lemma (in group) normal_inv_iff:
-     "(N \<lhd> G) <->
+     "(N \<lhd> G) \<longleftrightarrow>
       (subgroup(N,G) & (\<forall>x \<in> carrier(G). \<forall>h \<in> N. x \<cdot> h \<cdot> (inv x) \<in> N))"
-      (is "_ <-> ?rhs")
+      (is "_ \<longleftrightarrow> ?rhs")
 proof
   assume N: "N \<lhd> G"
   show ?rhs
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/LList.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -30,7 +30,7 @@
   standard pairs work just as well.  To use variant pairs, must change prefix
   a q/Q to the Sigma, Pair and converse rules.*)
 coinductive
-  domains "lleq(A)" <= "llist(A) * llist(A)"
+  domains "lleq(A)" \<subseteq> "llist(A) * llist(A)"
   intros
     LNil:  "<LNil, LNil> \<in> lleq(A)"
     LCons: "[| a \<in> A; <l,l'> \<in> lleq(A) |] 
@@ -74,7 +74,7 @@
 inductive_cases LConsE: "LCons(a,l) \<in> llist(A)"
 
 (*Proving freeness results*)
-lemma LCons_iff: "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"
+lemma LCons_iff: "LCons(a,l)=LCons(a',l') \<longleftrightarrow> a=a' & l=l'"
 by auto
 
 lemma LNil_LCons_iff: "~ LNil=LCons(a,l)"
@@ -107,7 +107,7 @@
 declare Ord_in_Ord [elim!]
 
 lemma llist_quniv_lemma [rule_format]:
-     "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l Int Vset(i) \<subseteq> univ(eclose(A))"
+     "Ord(i) ==> \<forall>l \<in> llist(quniv(A)). l \<inter> Vset(i) \<subseteq> univ(eclose(A))"
 apply (erule trans_induct)
 apply (rule ballI)
 apply (erule llist.cases)
@@ -135,7 +135,7 @@
 
 (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
 lemma lleq_Int_Vset_subset [rule_format]:
-     "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) --> l Int Vset(i) \<subseteq> l'"
+     "Ord(i) ==> \<forall>l l'. <l,l'> \<in> lleq(A) \<longrightarrow> l \<inter> Vset(i) \<subseteq> l'"
 apply (erule trans_induct)
 apply (intro allI impI)
 apply (erule lleq.cases)
@@ -200,7 +200,7 @@
         flip_LCons [simp] 
         not_type [simp]
 
-lemma bool_Int_subset_univ: "b \<in> bool ==> b Int X \<subseteq> univ(eclose(A))"
+lemma bool_Int_subset_univ: "b \<in> bool ==> b \<inter> X \<subseteq> univ(eclose(A))"
 by (fast intro: Int_lower1 [THEN subset_trans] elim!: boolE)
 
 declare not_type [intro!]
@@ -209,7 +209,7 @@
 (*Reasoning borrowed from lleq.ML; a similar proof works for all
   "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
 lemma flip_llist_quniv_lemma [rule_format]:
-     "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) Int Vset(i) \<subseteq> univ(eclose(bool))"
+     "Ord(i) ==> \<forall>l \<in> llist(bool). flip(l) \<inter> Vset(i) \<subseteq> univ(eclose(bool))"
 apply (erule trans_induct)
 apply (rule ballI)
 apply (erule llist.cases, simp_all)
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/Limit.thy
--- a/src/ZF/ex/Limit.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Limit.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -7,13 +7,13 @@
 The following paper comments on the formalization:
 
 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
-In Proceedings of the First Isabelle Users Workshop, Technical 
+In Proceedings of the First Isabelle Users Workshop, Technical
 Report No. 379, University of Cambridge Computer Laboratory, 1995.
 
 This is a condensed version of:
 
 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm
-Technical Report No. 369, University of Cambridge Computer 
+Technical Report No. 369, University of Cambridge Computer
 Laboratory, 1995.
 *)
 
@@ -32,8 +32,8 @@
     "po(D) ==
      (\<forall>x \<in> set(D). rel(D,x,x)) &
      (\<forall>x \<in> set(D). \<forall>y \<in> set(D). \<forall>z \<in> set(D).
-       rel(D,x,y) --> rel(D,y,z) --> rel(D,x,z)) &
-     (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) --> rel(D,y,x) --> x = y)"
+       rel(D,x,y) \<longrightarrow> rel(D,y,z) \<longrightarrow> rel(D,x,z)) &
+     (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longrightarrow> rel(D,y,x) \<longrightarrow> x = y)"
 
 definition
   chain :: "[i,i]=>o"  where
@@ -46,7 +46,7 @@
 
 definition
   islub :: "[i,i,i]=>o"  where
-    "islub(D,X,x) == isub(D,X,x) & (\<forall>y. isub(D,X,y) --> rel(D,x,y))"
+    "islub(D,X,x) == isub(D,X,x) & (\<forall>y. isub(D,X,y) \<longrightarrow> rel(D,x,y))"
 
 definition
   lub :: "[i,i]=>i"  where
@@ -54,7 +54,7 @@
 
 definition
   cpo :: "i=>o"  where
-    "cpo(D) == po(D) & (\<forall>X. chain(D,X) --> (\<exists>x. islub(D,X,x)))"
+    "cpo(D) == po(D) & (\<forall>X. chain(D,X) \<longrightarrow> (\<exists>x. islub(D,X,x)))"
 
 definition
   pcpo :: "i=>o"  where
@@ -68,13 +68,13 @@
   mono :: "[i,i]=>i"  where
     "mono(D,E) ==
      {f \<in> set(D)->set(E).
-      \<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) --> rel(E,f`x,f`y)}"
+      \<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longrightarrow> rel(E,f`x,f`y)}"
 
 definition
   cont :: "[i,i]=>i"  where
     "cont(D,E) ==
      {f \<in> mono(D,E).
-      \<forall>X. chain(D,X) --> f`(lub(D,X)) = lub(E,\<lambda>n \<in> nat. f`(X`n))}"
+      \<forall>X. chain(D,X) \<longrightarrow> f`(lub(D,X)) = lub(E,\<lambda>n \<in> nat. f`(X`n))}"
 
 definition
   cf :: "[i,i]=>i"  where
@@ -134,8 +134,8 @@
   subcpo    :: "[i,i]=>o"  where
     "subcpo(D,E) ==
      set(D) \<subseteq> set(E) &
-     (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) <-> rel(E,x,y)) &
-     (\<forall>X. chain(D,X) --> lub(E,X):set(D))"
+     (\<forall>x \<in> set(D). \<forall>y \<in> set(D). rel(D,x,y) \<longleftrightarrow> rel(E,x,y)) &
+     (\<forall>X. chain(D,X) \<longrightarrow> lub(E,X):set(D))"
 
 definition
   subpcpo   :: "[i,i]=>o"  where
@@ -154,13 +154,13 @@
 
 definition
   e_less    :: "[i,i,i,i]=>i"  where
-  (* Valid for m le n only. *)
+  (* Valid for m \<le> n only. *)
     "e_less(DD,ee,m,n) == rec(n#-m,id(set(DD`m)),%x y. ee`(m#+x) O y)"
 
 
 definition
   e_gr      :: "[i,i,i,i]=>i"  where
-  (* Valid for n le m only. *)
+  (* Valid for n \<le> m only. *)
     "e_gr(DD,ee,m,n) ==
      rec(m#-n,id(set(DD`n)),
          %x y. y O Rp(DD`(n#+x),DD`(succ(n#+x)),ee`(n#+x)))"
@@ -168,7 +168,7 @@
 
 definition
   eps       :: "[i,i,i,i]=>i"  where
-    "eps(DD,ee,m,n) == if(m le n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"
+    "eps(DD,ee,m,n) == if(m \<le> n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"
 
 definition
   rho_emb   :: "[i,i,i]=>i"  where
@@ -182,7 +182,7 @@
   commute   :: "[i,i,i,i=>i]=>o"  where
     "commute(DD,ee,E,r) ==
      (\<forall>n \<in> nat. emb(DD`n,E,r(n))) &
-     (\<forall>m \<in> nat. \<forall>n \<in> nat. m le n --> r(n) O eps(DD,ee,m,n) = r(m))"
+     (\<forall>m \<in> nat. \<forall>n \<in> nat. m \<le> n \<longrightarrow> r(n) O eps(DD,ee,m,n) = r(m))"
 
 definition
   mediating :: "[i,i,i=>i,i=>i,i]=>o"  where
@@ -224,7 +224,7 @@
   "[| !!x. x \<in> set(D) ==> rel(D,x,x);
       !!x y z. [| rel(D,x,y); rel(D,y,z); x \<in> set(D); y \<in> set(D); z \<in> set(D)|]
                ==> rel(D,x,z);
-      !!x y. [| rel(D,x,y); rel(D,y,x); x \<in> set(D); y \<in> set(D)|] ==> x=y |] 
+      !!x y. [| rel(D,x,y); rel(D,y,x); x \<in> set(D); y \<in> set(D)|] ==> x=y |]
    ==> po(D)"
 by (unfold po_def, blast)
 
@@ -323,7 +323,7 @@
 done
 
 lemma chain_rel_gen:
-    "[|n le m; chain(D,X); cpo(D); m \<in> nat|] ==> rel(D,X`n,X`m)"
+    "[|n \<le> m; chain(D,X); cpo(D); m \<in> nat|] ==> rel(D,X`n,X`m)"
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (erule rev_mp) (*prepare the induction*)
 apply (induct_tac m)
@@ -382,14 +382,14 @@
 (*----------------------------------------------------------------------*)
 
 lemma isub_suffix:
-    "[| chain(D,X); cpo(D) |] ==> isub(D,suffix(X,n),x) <-> isub(D,X,x)"
+    "[| chain(D,X); cpo(D) |] ==> isub(D,suffix(X,n),x) \<longleftrightarrow> isub(D,X,x)"
 apply (simp add: isub_def suffix_def, safe)
 apply (drule_tac x = na in bspec)
 apply (auto intro: cpo_trans chain_rel_gen_add)
 done
 
 lemma islub_suffix:
-  "[|chain(D,X); cpo(D)|] ==> islub(D,suffix(X,n),x) <-> islub(D,X,x)"
+  "[|chain(D,X); cpo(D)|] ==> islub(D,suffix(X,n),x) \<longleftrightarrow> islub(D,X,x)"
 by (simp add: islub_def isub_suffix)
 
 lemma lub_suffix:
@@ -401,7 +401,7 @@
 (*----------------------------------------------------------------------*)
 
 lemma dominateI:
-  "[| !!m. m \<in> nat ==> n(m):nat; !!m. m \<in> nat ==> rel(D,X`m,Y`n(m))|] 
+  "[| !!m. m \<in> nat ==> n(m):nat; !!m. m \<in> nat ==> rel(D,X`m,Y`n(m))|]
    ==> dominate(D,X,Y)"
 by (simp add: dominate_def, blast)
 
@@ -426,7 +426,7 @@
 lemma dominate_islub_eq:
      "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D);
         X \<in> nat->set(D); Y \<in> nat->set(D)|] ==> x = y"
-by (blast intro: cpo_antisym dominate_islub islub_least subchain_isub 
+by (blast intro: cpo_antisym dominate_islub islub_least subchain_isub
                  islub_isub islub_in)
 
 
@@ -488,19 +488,19 @@
   shows "matrix(D,M)"
 proof -
   {
-    fix n m assume "n : nat" "m : nat"
+    fix n m assume "n \<in> nat" "m \<in> nat"
     with chain_rel [OF yprem]
     have "rel(D, M ` n ` m, M ` succ(n) ` m)" by simp
   } note rel_succ = this
   show "matrix(D,M)"
   proof (simp add: matrix_def Mfun rel_succ, intro conjI ballI)
-    fix n m assume n: "n : nat" and m: "m : nat"
+    fix n m assume n: "n \<in> nat" and m: "m \<in> nat"
     thus "rel(D, M ` n ` m, M ` n ` succ(m))"
       by (simp add: chain_rel xprem)
   next
-    fix n m assume n: "n : nat" and m: "m : nat"
+    fix n m assume n: "n \<in> nat" and m: "m \<in> nat"
     thus "rel(D, M ` n ` m, M ` succ(n) ` succ(m))"
-      by (rule cpo_trans [OF cpoD rel_succ], 
+      by (rule cpo_trans [OF cpoD rel_succ],
           simp_all add: chain_fun [THEN apply_type] xprem)
   qed
 qed
@@ -511,31 +511,31 @@
 by simp
 
 lemma isub_lemma:
-    "[|isub(D, \<lambda>n \<in> nat. M`n`n, y); matrix(D,M); cpo(D)|] 
+    "[|isub(D, \<lambda>n \<in> nat. M`n`n, y); matrix(D,M); cpo(D)|]
      ==> isub(D, \<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m), y)"
 proof (simp add: isub_def, safe)
   fix n
-  assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \<in> nat" and y: "y \<in> set(D)" 
+  assume DM: "matrix(D, M)" and D: "cpo(D)" and n: "n \<in> nat" and y: "y \<in> set(D)"
      and rel: "\<forall>n\<in>nat. rel(D, M ` n ` n, y)"
   have "rel(D, lub(D, M ` n), y)"
   proof (rule matrix_chain_left [THEN cpo_lub, THEN islub_least], simp_all add: n D DM)
-    show "isub(D, M ` n, y)" 
+    show "isub(D, M ` n, y)"
       proof (unfold isub_def, intro conjI ballI y)
         fix k assume k: "k \<in> nat"
         show "rel(D, M ` n ` k, y)"
-          proof (cases "n le k")
-            case True 
-            hence yy: "rel(D, M`n`k, M`k`k)" 
-              by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right) 
+          proof (cases "n \<le> k")
+            case True
+            hence yy: "rel(D, M`n`k, M`k`k)"
+              by (blast intro: lemma2 n k y DM D chain_rel_gen matrix_chain_right)
             show "?thesis"
-              by (rule cpo_trans [OF D yy], 
+              by (rule cpo_trans [OF D yy],
                   simp_all add: k rel n y DM matrix_in)
           next
             case False
-            hence le: "k le n" 
-              by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k) 
+            hence le: "k \<le> n"
+              by (blast intro: not_le_iff_lt [THEN iffD1, THEN leI] nat_into_Ord n k)
             show "?thesis"
-              by (rule cpo_trans [OF D chain_rel_gen [OF le]], 
+              by (rule cpo_trans [OF D chain_rel_gen [OF le]],
                   simp_all add: n y k rel DM D matrix_chain_left)
           qed
         qed
@@ -550,7 +550,7 @@
 proof (simp add: chain_def, intro conjI ballI)
   assume "matrix(D, M)" "cpo(D)"
   thus "(\<lambda>x\<in>nat. lub(D, Lambda(nat, op `(M ` x)))) \<in> nat \<rightarrow> set(D)"
-    by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1) 
+    by (force intro: islub_in cpo_lub chainI lam_type matrix_in matrix_rel_0_1)
 next
   fix n
   assume DD: "matrix(D, M)" "cpo(D)" "n \<in> nat"
@@ -558,24 +558,24 @@
     by (force simp add: dominate_def intro: matrix_rel_1_0)
   with DD show "rel(D, lub(D, Lambda(nat, op `(M ` n))),
                lub(D, Lambda(nat, op `(M ` succ(n)))))"
-    by (simp add: matrix_chain_left [THEN chain_fun, THEN eta] 
+    by (simp add: matrix_chain_left [THEN chain_fun, THEN eta]
       dominate_islub cpo_lub matrix_chain_left chain_fun)
 qed
 
 lemma isub_eq:
   assumes DM: "matrix(D, M)" and D: "cpo(D)"
-  shows "isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) <-> isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
+  shows "isub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m)),y) \<longleftrightarrow> isub(D,(\<lambda>n \<in> nat. M`n`n),y)"
 proof
   assume isub: "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)"
-  hence dom: "dominate(D, \<lambda>n\<in>nat. M ` n ` n, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))))" 
+  hence dom: "dominate(D, \<lambda>n\<in>nat. M ` n ` n, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))))"
     using DM D
     by (simp add: dominate_def, intro ballI bexI,
         simp_all add: matrix_chain_left [THEN chain_fun, THEN eta] islub_ub cpo_lub matrix_chain_left)
   thus "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)" using DM D
-    by - (rule dominate_isub [OF dom isub], 
+    by - (rule dominate_isub [OF dom isub],
           simp_all add: matrix_chain_diag chain_fun matrix_chain_lub)
 next
-  assume isub: "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)" 
+  assume isub: "isub(D, \<lambda>n\<in>nat. M ` n ` n, y)"
   thus "isub(D, \<lambda>n\<in>nat. lub(D, Lambda(nat, op `(M ` n))), y)"  using DM D
     by (simp add: isub_lemma)
 qed
@@ -591,7 +591,7 @@
 by (simp add: lub_def)
 
 lemma lub_matrix_diag:
-    "[|matrix(D,M); cpo(D)|] 
+    "[|matrix(D,M); cpo(D)|]
      ==> lub(D,(\<lambda>n \<in> nat. lub(D,\<lambda>m \<in> nat. M`n`m))) =
          lub(D,(\<lambda>n \<in> nat. M`n`n))"
 apply (simp (no_asm) add: lub_matrix_diag_aux1 lub_matrix_diag_aux2)
@@ -599,7 +599,7 @@
 done
 
 lemma lub_matrix_diag_sym:
-    "[|matrix(D,M); cpo(D)|] 
+    "[|matrix(D,M); cpo(D)|]
      ==> lub(D,(\<lambda>m \<in> nat. lub(D,\<lambda>n \<in> nat. M`n`m))) =
          lub(D,(\<lambda>n \<in> nat. M`n`n))"
 by (drule matrix_sym_axis [THEN lub_matrix_diag], auto)
@@ -610,7 +610,7 @@
 
 lemma monoI:
     "[|f \<in> set(D)->set(E);
-       !!x y. [|rel(D,x,y); x \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y)|] 
+       !!x y. [|rel(D,x,y); x \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y)|]
      ==> f \<in> mono(D,E)"
 by (simp add: mono_def)
 
@@ -627,14 +627,14 @@
 lemma contI:
     "[|f \<in> set(D)->set(E);
        !!x y. [|rel(D,x,y); x \<in> set(D); y \<in> set(D)|] ==> rel(E,f`x,f`y);
-       !!X. chain(D,X) ==> f`lub(D,X) = lub(E,\<lambda>n \<in> nat. f`(X`n))|] 
+       !!X. chain(D,X) ==> f`lub(D,X) = lub(E,\<lambda>n \<in> nat. f`(X`n))|]
      ==> f \<in> cont(D,E)"
 by (simp add: cont_def mono_def)
 
 lemma cont2mono: "f \<in> cont(D,E) ==> f \<in> mono(D,E)"
 by (simp add: cont_def)
 
-lemma cont_fun [TC] : "f \<in> cont(D,E) ==> f \<in> set(D)->set(E)"
+lemma cont_fun [TC]: "f \<in> cont(D,E) ==> f \<in> set(D)->set(E)"
 apply (simp add: cont_def)
 apply (rule mono_fun, blast)
 done
@@ -684,7 +684,7 @@
 (* rel_cf originally an equality. Now stated as two rules. Seemed easiest. *)
 
 lemma rel_cfI:
-    "[|!!x. x \<in> set(D) ==> rel(E,f`x,g`x); f \<in> cont(D,E); g \<in> cont(D,E)|] 
+    "[|!!x. x \<in> set(D) ==> rel(E,f`x,g`x); f \<in> cont(D,E); g \<in> cont(D,E)|]
      ==> rel(cf(D,E),f,g)"
 by (simp add: rel_I cf_def)
 
@@ -703,7 +703,7 @@
 done
 
 lemma matrix_lemma:
-    "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |] 
+    "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |]
      ==> matrix(E,\<lambda>x \<in> nat. \<lambda>xa \<in> nat. X`x`(Xa`xa))"
 apply (rule matrix_chainI, auto)
 apply (force intro: chainI lam_type apply_funtype cont_fun cf_cont cont_mono)
@@ -716,13 +716,13 @@
   shows   "(\<lambda>x \<in> set(D). lub(E, \<lambda>n \<in> nat. X ` n ` x)) \<in> cont(D, E)"
 proof (rule contI)
   show "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) \<in> set(D) \<rightarrow> set(E)"
-    by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E) 
+    by (blast intro: lam_type chain_cf [THEN cpo_lub, THEN islub_in] ch E)
 next
   fix x y
   assume xy: "rel(D, x, y)" "x \<in> set(D)" "y \<in> set(D)"
   hence dom: "dominate(E, \<lambda>n\<in>nat. X ` n ` x, \<lambda>n\<in>nat. X ` n ` y)"
     by (force intro: dominateI  chain_in [OF ch, THEN cf_cont, THEN cont_mono])
-  note chE = chain_cf [OF ch] 
+  note chE = chain_cf [OF ch]
   from xy show "rel(E, (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` x,
                        (\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` y)"
     by (simp add: dominate_islub [OF dom] cpo_lub [OF chE] E chain_fun [OF chE])
@@ -735,7 +735,7 @@
     by (simp add: D E)
    also have "... =  lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))"
     using  matrix_lemma [THEN lub_matrix_diag_sym, OF ch chDY]
-    by (simp add: D E) 
+    by (simp add: D E)
   finally have "lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` x ` (Y ` n))) =
                 lub(E, \<lambda>x\<in>nat. lub(E, \<lambda>n\<in>nat. X ` n ` (Y ` x)))" .
   thus "(\<lambda>x\<in>set(D). lub(E, \<lambda>n\<in>nat. X ` n ` x)) ` lub(D, Y) =
@@ -745,7 +745,7 @@
   qed
 
 lemma islub_cf:
-    "[| chain(cf(D,E),X); cpo(D); cpo(E)|] 
+    "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
      ==> islub(cf(D,E), X, \<lambda>x \<in> set(D). lub(E,\<lambda>n \<in> nat. X`n`x))"
 apply (rule islubI)
 apply (rule isubI)
@@ -774,13 +774,13 @@
 apply (assumption | rule cf_cont [THEN cont_fun, THEN apply_type] cf_cont)+
 apply (rule fun_extension)
 apply (assumption | rule cf_cont [THEN cont_fun])+
-apply (blast intro: cpo_antisym rel_cf 
+apply (blast intro: cpo_antisym rel_cf
                     cf_cont [THEN cont_fun, THEN apply_type])
 apply (fast intro: islub_cf)
 done
 
 lemma lub_cf:
-     "[| chain(cf(D,E),X); cpo(D); cpo(E)|] 
+     "[| chain(cf(D,E),X); cpo(D); cpo(E)|]
       ==> lub(cf(D,E), X) = (\<lambda>x \<in> set(D). lub(E,\<lambda>n \<in> nat. X`n`x))"
 by (blast intro: islub_unique cpo_lub islub_cf cpo_cf)
 
@@ -801,13 +801,13 @@
 lemma pcpo_cf:
     "[|cpo(D); pcpo(E)|] ==> pcpo(cf(D,E))"
 apply (rule pcpoI)
-apply (assumption | 
+apply (assumption |
        rule cf_least bot_in const_cont [THEN cont_cf] cf_cont cpo_cf pcpo_cpo)+
 done
 
 lemma bot_cf:
     "[|cpo(D); pcpo(E)|] ==> bot(cf(D,E)) = (\<lambda>x \<in> set(D).bot(E))"
-by (blast intro: bot_unique [symmetric] pcpo_cf cf_least 
+by (blast intro: bot_unique [symmetric] pcpo_cf cf_least
                  bot_in [THEN const_cont, THEN cont_cf] cf_cont pcpo_cpo)
 
 (*----------------------------------------------------------------------*)
@@ -838,9 +838,9 @@
 
 lemma comp_mono:
     "[| f \<in> cont(D',E); g \<in> cont(D,D'); f':cont(D',E); g':cont(D,D');
-        rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |] 
+        rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |]
      ==> rel(cf(D,E),f O g,f' O g')"
-apply (rule rel_cfI) 
+apply (rule rel_cfI)
 apply (subst comp_cont_apply)
 apply (rule_tac [3] comp_cont_apply [THEN ssubst])
 apply (rule_tac [5] cpo_trans)
@@ -848,7 +848,7 @@
 done
 
 lemma chain_cf_comp:
-    "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(E)|] 
+    "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(E)|]
      ==> chain(cf(D,E),\<lambda>n \<in> nat. X`n O Y`n)"
 apply (rule chainI)
 defer 1
@@ -858,23 +858,23 @@
 apply (rule_tac [3] comp_cont_apply [THEN ssubst])
 apply (rule_tac [5] cpo_trans)
 apply (rule_tac [6] rel_cf)
-apply (rule_tac [8] cont_mono) 
-apply (blast intro: lam_type comp_pres_cont cont_cf chain_in [THEN cf_cont] 
+apply (rule_tac [8] cont_mono)
+apply (blast intro: lam_type comp_pres_cont cont_cf chain_in [THEN cf_cont]
                     cont_map chain_rel rel_cf)+
 done
 
 lemma comp_lubs:
-    "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(D'); cpo(E)|] 
+    "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(D'); cpo(E)|]
      ==> lub(cf(D',E),X) O lub(cf(D,D'),Y) = lub(cf(D,E),\<lambda>n \<in> nat. X`n O Y`n)"
 apply (rule fun_extension)
 apply (rule_tac [3] lub_cf [THEN ssubst])
-apply (assumption | 
-       rule comp_fun cf_cont [THEN cont_fun]  cpo_lub [THEN islub_in]  
+apply (assumption |
+       rule comp_fun cf_cont [THEN cont_fun]  cpo_lub [THEN islub_in]
             cpo_cf chain_cf_comp)+
 apply (simp add: chain_in [THEN cf_cont, THEN comp_cont_apply])
 apply (subst comp_cont_apply)
 apply (assumption | rule cpo_lub [THEN islub_in, THEN cf_cont]  cpo_cf)+
-apply (simp add: lub_cf chain_cf chain_in [THEN cf_cont, THEN cont_lub] 
+apply (simp add: lub_cf chain_cf chain_in [THEN cf_cont, THEN cont_lub]
                  chain_cf [THEN cpo_lub, THEN islub_in])
 apply (cut_tac M = "\<lambda>xa \<in> nat. \<lambda>xb \<in> nat. X`xa` (Y`xb`x)" in lub_matrix_diag)
 prefer 3 apply simp
@@ -968,8 +968,8 @@
 
 
 lemma projpair_unique:
-    "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|] 
-     ==> (e=e')<->(p=p')"
+    "[|cpo(D); cpo(E); projpair(D,E,e,p); projpair(D,E,e',p')|]
+     ==> (e=e')\<longleftrightarrow>(p=p')"
 by (blast intro: cpo_antisym projpair_unique_aux1 projpair_unique_aux2 cpo_cf cont_cf
           dest: projpair_ep_cont)
 
@@ -1036,7 +1036,7 @@
 (* Proof in Isa/ZF: 23 lines (compared to 56: 60% reduction). *)
 
 lemma comp_lemma:
-    "[|emb(D,D',e); emb(D',E,e'); cpo(D); cpo(D'); cpo(E)|] 
+    "[|emb(D,D',e); emb(D',E,e'); cpo(D); cpo(D'); cpo(E)|]
      ==> projpair(D,E,e' O e,(Rp(D,D',e)) O (Rp(D',E,e')))"
 apply (simp add: projpair_def, safe)
 apply (assumption | rule comp_pres_cont Rp_cont emb_cont)+
@@ -1090,7 +1090,7 @@
 by (simp add: iprod_def rel_def)
 
 lemma chain_iprod:
-    "[|chain(iprod(DD),X);  !!n. n \<in> nat ==> cpo(DD`n); n \<in> nat|] 
+    "[|chain(iprod(DD),X);  !!n. n \<in> nat ==> cpo(DD`n); n \<in> nat|]
      ==> chain(DD`n,\<lambda>m \<in> nat. X`m`n)"
 apply (unfold chain_def, safe)
 apply (rule lam_type)
@@ -1101,7 +1101,7 @@
 done
 
 lemma islub_iprod:
-    "[|chain(iprod(DD),X);  !!n. n \<in> nat ==> cpo(DD`n)|] 
+    "[|chain(iprod(DD),X);  !!n. n \<in> nat ==> cpo(DD`n)|]
      ==> islub(iprod(DD),X,\<lambda>n \<in> nat. lub(DD`n,\<lambda>m \<in> nat. X`m`n))"
 apply (simp add: islub_def isub_def, safe)
 apply (rule iprodI)
@@ -1151,7 +1151,7 @@
 
 lemma subcpoI:
     "[|set(D)<=set(E);
-       !!x y. [|x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)<->rel(E,x,y);
+       !!x y. [|x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)\<longleftrightarrow>rel(E,x,y);
        !!X. chain(D,X) ==> lub(E,X) \<in> set(D)|] ==> subcpo(D,E)"
 by (simp add: subcpo_def)
 
@@ -1159,7 +1159,7 @@
 by (simp add: subcpo_def)
 
 lemma subcpo_rel_eq:
-    "[|subcpo(D,E); x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)<->rel(E,x,y)"
+    "[|subcpo(D,E); x \<in> set(D); y \<in> set(D)|] ==> rel(D,x,y)\<longleftrightarrow>rel(E,x,y)"
 by (simp add: subcpo_def)
 
 lemmas subcpo_relD1 = subcpo_rel_eq [THEN iffD1]
@@ -1213,7 +1213,7 @@
 by (simp add: rel_def mkcpo_def)
 
 lemma rel_mkcpo:
-    "[|x \<in> set(D); y \<in> set(D)|] ==> rel(mkcpo(D,P),x,y) <-> rel(D,x,y)"
+    "[|x \<in> set(D); y \<in> set(D)|] ==> rel(mkcpo(D,P),x,y) \<longleftrightarrow> rel(D,x,y)"
 by (simp add: mkcpo_def rel_def set_def)
 
 lemma chain_mkcpo:
@@ -1273,7 +1273,7 @@
 
 lemma rel_DinfI:
     "[|!!n. n \<in> nat ==> rel(DD`n,x`n,y`n);
-       x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|] 
+       x:(\<Pi> n \<in> nat. set(DD`n)); y:(\<Pi> n \<in> nat. set(DD`n))|]
      ==> rel(Dinf(DD,ee),x,y)"
 apply (simp add: Dinf_def)
 apply (blast intro: rel_mkcpo [THEN iffD2] rel_iprodI iprodI)
@@ -1299,7 +1299,7 @@
 apply (assumption | rule chain_Dinf emb_chain_cpo)+
 apply simp
 apply (subst Rp_cont [THEN cont_lub])
-apply (assumption | 
+apply (assumption |
        rule emb_chain_cpo emb_chain_emb nat_succI chain_iprod chain_Dinf)+
 (* Useful simplification, ugly in HOL. *)
 apply (simp add: Dinf_eq chain_in)
@@ -1341,11 +1341,11 @@
 by (simp add: e_less_def)
 
 lemma le_exists:
-    "[| m le n;  !!x. [|n=m#+x; x \<in> nat|] ==> Q;  n \<in> nat |] ==> Q"
+    "[| m \<le> n;  !!x. [|n=m#+x; x \<in> nat|] ==> Q;  n \<in> nat |] ==> Q"
 apply (drule less_imp_succ_add, auto)
 done
 
-lemma e_less_le: "[| m le n;  n \<in> nat |] 
+lemma e_less_le: "[| m \<le> n;  n \<in> nat |]
      ==> e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)"
 apply (rule le_exists, assumption)
 apply (simp add: e_less_add, assumption)
@@ -1358,7 +1358,7 @@
 by (simp add: e_less_le e_less_eq)
 
 lemma e_less_succ_emb:
-    "[|!!n. n \<in> nat ==> emb(DD`n,DD`succ(n),ee`n); m \<in> nat|] 
+    "[|!!n. n \<in> nat ==> emb(DD`n,DD`succ(n),ee`n); m \<in> nat|]
      ==> e_less(DD,ee,m,succ(m)) = ee`m"
 apply (simp add: e_less_succ)
 apply (blast intro: emb_cont cont_fun comp_id)
@@ -1370,7 +1370,7 @@
 lemma emb_e_less_add:
      "[| emb_chain(DD,ee); m \<in> nat |]
       ==> emb(DD`m, DD`(m#+k), e_less(DD,ee,m,m#+k))"
-apply (subgoal_tac "emb (DD`m, DD` (m#+natify (k)), 
+apply (subgoal_tac "emb (DD`m, DD` (m#+natify (k)),
                          e_less (DD,ee,m,m#+natify (k))) ")
 apply (rule_tac [2] n = "natify (k) " in nat_induct)
 apply (simp_all add: e_less_eq)
@@ -1380,7 +1380,7 @@
 done
 
 lemma emb_e_less:
-     "[| m le n;  emb_chain(DD,ee);  n \<in> nat |] 
+     "[| m \<le> n;  emb_chain(DD,ee);  n \<in> nat |]
       ==> emb(DD`m, DD`n, e_less(DD,ee,m,n))"
 apply (frule lt_nat_in_nat)
 apply (erule nat_succI)
@@ -1397,8 +1397,8 @@
    Therefore this theorem is only a lemma. *)
 
 lemma e_less_split_add_lemma [rule_format]:
-    "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
-     ==> n le k -->
+    "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+     ==> n \<le> k \<longrightarrow>
          e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)"
 apply (induct_tac k)
 apply (simp add: e_less_eq id_type [THEN id_comp])
@@ -1419,7 +1419,7 @@
 done
 
 lemma e_less_split_add:
-    "[| n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[| n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)"
 by (blast intro: e_less_split_add_lemma)
 
@@ -1428,13 +1428,13 @@
 by (simp add: e_gr_def)
 
 lemma e_gr_add:
-    "[|n \<in> nat; k \<in> nat|] 
+    "[|n \<in> nat; k \<in> nat|]
      ==> e_gr(DD,ee,succ(n#+k),n) =
          e_gr(DD,ee,n#+k,n) O Rp(DD`(n#+k),DD`succ(n#+k),ee`(n#+k))"
 by (simp add: e_gr_def)
 
 lemma e_gr_le:
-     "[|n le m; m \<in> nat; n \<in> nat|]
+     "[|n \<le> m; m \<in> nat; n \<in> nat|]
       ==> e_gr(DD,ee,succ(m),n) = e_gr(DD,ee,m,n) O Rp(DD`m,DD`succ(m),ee`m)"
 apply (erule le_exists)
 apply (simp add: e_gr_add, assumption+)
@@ -1445,14 +1445,14 @@
 by (simp add: e_gr_le e_gr_eq)
 
 (* Cpo asm's due to THE uniqueness. *)
-lemma e_gr_succ_emb: "[|emb_chain(DD,ee); m \<in> nat|] 
+lemma e_gr_succ_emb: "[|emb_chain(DD,ee); m \<in> nat|]
      ==> e_gr(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)"
 apply (simp add: e_gr_succ)
 apply (blast intro: id_comp Rp_cont cont_fun emb_chain_cpo emb_chain_emb)
 done
 
 lemma e_gr_fun_add:
-    "[|emb_chain(DD,ee); n \<in> nat; k \<in> nat|] 
+    "[|emb_chain(DD,ee); n \<in> nat; k \<in> nat|]
      ==> e_gr(DD,ee,n#+k,n): set(DD`(n#+k))->set(DD`n)"
 apply (induct_tac k)
 apply (simp add: e_gr_eq id_type)
@@ -1461,15 +1461,15 @@
 done
 
 lemma e_gr_fun:
-    "[|n le m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|] 
+    "[|n \<le> m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
      ==> e_gr(DD,ee,m,n): set(DD`m)->set(DD`n)"
 apply (rule le_exists, assumption)
 apply (simp add: e_gr_fun_add, assumption+)
 done
 
 lemma e_gr_split_add_lemma:
-    "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
-     ==> m le k -->
+    "[| emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
+     ==> m \<le> k \<longrightarrow>
          e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)"
 apply (induct_tac k)
 apply (rule impI)
@@ -1491,19 +1491,19 @@
 done
 
 lemma e_gr_split_add:
-     "[| m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+     "[| m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
       ==> e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)"
 apply (blast intro: e_gr_split_add_lemma [THEN mp])
 done
 
 lemma e_less_cont:
-     "[|m le n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|] 
+     "[|m \<le> n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
       ==> e_less(DD,ee,m,n):cont(DD`m,DD`n)"
 apply (blast intro: emb_cont emb_e_less)
 done
 
 lemma e_gr_cont:
-    "[|n le m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|] 
+    "[|n \<le> m; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
      ==> e_gr(DD,ee,m,n):cont(DD`m,DD`n)"
 apply (erule rev_mp)
 apply (induct_tac m)
@@ -1520,7 +1520,7 @@
 (* Considerably shorter.... 57 against 26 *)
 
 lemma e_less_e_gr_split_add:
-    "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> e_less(DD,ee,m,m#+n) = e_gr(DD,ee,m#+k,m#+n) O e_less(DD,ee,m,m#+k)"
 (* Use mp to prepare for induction. *)
 apply (erule rev_mp)
@@ -1547,7 +1547,7 @@
 (* Again considerably shorter, and easy to obtain from the previous thm. *)
 
 lemma e_gr_e_less_split_add:
-    "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> e_gr(DD,ee,n#+m,n) = e_gr(DD,ee,n#+k,n) O e_less(DD,ee,n#+m,n#+k)"
 (* Use mp to prepare for induction. *)
 apply (erule rev_mp)
@@ -1572,7 +1572,7 @@
 
 
 lemma emb_eps:
-    "[|m le n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
+    "[|m \<le> n; emb_chain(DD,ee); m \<in> nat; n \<in> nat|]
      ==> emb(DD`m,DD`n,eps(DD,ee,m,n))"
 apply (simp add: eps_def)
 apply (blast intro: emb_e_less)
@@ -1595,7 +1595,7 @@
 by (simp add: eps_def add_le_self)
 
 lemma eps_e_less:
-    "[|m le n; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_less(DD,ee,m,n)"
+    "[|m \<le> n; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_less(DD,ee,m,n)"
 by (simp add: eps_def)
 
 lemma eps_e_gr_add:
@@ -1603,7 +1603,7 @@
 by (simp add: eps_def e_less_eq e_gr_eq)
 
 lemma eps_e_gr:
-    "[|n le m; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_gr(DD,ee,m,n)"
+    "[|n \<le> m; m \<in> nat; n \<in> nat|] ==> eps(DD,ee,m,n) = e_gr(DD,ee,m,n)"
 apply (erule le_exists)
 apply (simp_all add: eps_e_gr_add)
 done
@@ -1627,28 +1627,28 @@
 (* Theorems about splitting. *)
 
 lemma eps_split_add_left:
-    "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,m#+k) = eps(DD,ee,m#+n,m#+k) O eps(DD,ee,m,m#+n)"
 apply (simp add: eps_e_less add_le_self add_le_mono)
 apply (auto intro: e_less_split_add)
 done
 
 lemma eps_split_add_left_rev:
-    "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,m#+n) = eps(DD,ee,m#+k,m#+n) O eps(DD,ee,m,m#+k)"
 apply (simp add: eps_e_less_add eps_e_gr add_le_self add_le_mono)
 apply (auto intro: e_less_e_gr_split_add)
 done
 
 lemma eps_split_add_right:
-    "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,n#+k,n) = eps(DD,ee,n#+m,n) O eps(DD,ee,n#+k,n#+m)"
 apply (simp add: eps_e_gr add_le_self add_le_mono)
 apply (auto intro: e_gr_split_add)
 done
 
 lemma eps_split_add_right_rev:
-    "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,n#+m,n) = eps(DD,ee,n#+k,n) O eps(DD,ee,n#+m,n#+k)"
 apply (simp add: eps_e_gr_add eps_e_less add_le_self add_le_mono)
 apply (auto intro: e_gr_e_less_split_add)
@@ -1657,8 +1657,8 @@
 (* Arithmetic *)
 
 lemma le_exists_lemma:
-    "[| n le k; k le m;
-        !!p q. [|p le q; k=n#+p; m=n#+q; p \<in> nat; q \<in> nat|] ==> R;
+    "[| n \<le> k; k \<le> m;
+        !!p q. [|p \<le> q; k=n#+p; m=n#+q; p \<in> nat; q \<in> nat|] ==> R;
         m \<in> nat |]==>R"
 apply (rule le_exists, assumption)
 prefer 2 apply (simp add: lt_nat_in_nat)
@@ -1666,28 +1666,28 @@
 done
 
 lemma eps_split_left_le:
-    "[|m le k; k le n; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|m \<le> k; k \<le> n; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
 apply (rule le_exists_lemma, assumption+)
 apply (auto intro: eps_split_add_left)
 done
 
 lemma eps_split_left_le_rev:
-    "[|m le n; n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|m \<le> n; n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
 apply (rule le_exists_lemma, assumption+)
 apply (auto intro: eps_split_add_left_rev)
 done
 
 lemma eps_split_right_le:
-    "[|n le k; k le m; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|n \<le> k; k \<le> m; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
 apply (rule le_exists_lemma, assumption+)
 apply (auto intro: eps_split_add_right)
 done
 
 lemma eps_split_right_le_rev:
-    "[|n le m; m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|n \<le> m; m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
 apply (rule le_exists_lemma, assumption+)
 apply (auto intro: eps_split_add_right_rev)
@@ -1696,7 +1696,7 @@
 (* The desired two theorems about `splitting'. *)
 
 lemma eps_split_left:
-    "[|m le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|m \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
 apply (rule nat_linear_le)
 apply (rule_tac [4] eps_split_right_le_rev)
@@ -1708,7 +1708,7 @@
 done
 
 lemma eps_split_right:
-    "[|n le k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|] 
+    "[|n \<le> k; emb_chain(DD,ee); m \<in> nat; n \<in> nat; k \<in> nat|]
      ==> eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)"
 apply (rule nat_linear_le)
 apply (rule_tac [3] eps_split_left_le_rev)
@@ -1726,7 +1726,7 @@
 (* Considerably shorter. *)
 
 lemma rho_emb_fun:
-    "[|emb_chain(DD,ee); n \<in> nat|] 
+    "[|emb_chain(DD,ee); n \<in> nat|]
      ==> rho_emb(DD,ee,n): set(DD`n) -> set(Dinf(DD,ee))"
 apply (simp add: rho_emb_def)
 apply (assumption |
@@ -1742,8 +1742,8 @@
      apply (assumption | rule add_le_self nat_0I nat_succI)+
  apply (simp add: eps_succ_Rp)
  apply (subst comp_fun_apply)
-    apply (assumption | 
-           rule eps_fun nat_succI Rp_cont [THEN cont_fun] 
+    apply (assumption |
+           rule eps_fun nat_succI Rp_cont [THEN cont_fun]
                 emb_chain_emb emb_chain_cpo refl)+
 (* Now the second part of the proof. Slightly different than HOL. *)
 apply (simp add: eps_e_less nat_succI)
@@ -1752,7 +1752,7 @@
 apply (subst comp_fun_apply)
 apply (assumption | rule e_less_cont cont_fun emb_chain_emb emb_cont)+
 apply (subst embRp_eq_thm)
-apply (assumption | 
+apply (assumption |
        rule emb_chain_emb e_less_cont [THEN cont_fun, THEN apply_type]
             emb_chain_cpo nat_succI)+
  apply (simp add: eps_e_less)
@@ -1773,13 +1773,13 @@
 (* Shorter proof, 23 against 62. *)
 
 lemma rho_emb_cont:
-    "[|emb_chain(DD,ee); n \<in> nat|] 
+    "[|emb_chain(DD,ee); n \<in> nat|]
      ==> rho_emb(DD,ee,n): cont(DD`n,Dinf(DD,ee))"
 apply (rule contI)
 apply (assumption | rule rho_emb_fun)+
 apply (rule rel_DinfI)
 apply (simp add: rho_emb_def)
-apply (assumption | 
+apply (assumption |
        rule eps_cont [THEN cont_mono]  Dinf_prod apply_type rho_emb_fun)+
 (* Continuity, different order, slightly different proofs. *)
 apply (subst lub_Dinf)
@@ -1788,16 +1788,16 @@
 apply simp
 apply (rule rel_DinfI)
 apply (simp add: rho_emb_apply2 chain_in)
-apply (assumption | 
-       rule eps_cont [THEN cont_mono]  chain_rel Dinf_prod 
+apply (assumption |
+       rule eps_cont [THEN cont_mono]  chain_rel Dinf_prod
             rho_emb_fun [THEN apply_type]  chain_in nat_succI)+
 (* Now, back to the result of applying lub_Dinf *)
 apply (simp add: rho_emb_apply2 chain_in)
 apply (subst rho_emb_apply1)
 apply (assumption | rule cpo_lub [THEN islub_in]  emb_chain_cpo)+
 apply (rule fun_extension)
-apply (assumption | 
-       rule lam_type eps_cont [THEN cont_fun, THEN apply_type]  
+apply (assumption |
+       rule lam_type eps_cont [THEN cont_fun, THEN apply_type]
             cpo_lub [THEN islub_in]  emb_chain_cpo)+
 apply (assumption | rule cont_chain eps_cont emb_chain_cpo)+
 apply simp
@@ -1807,7 +1807,7 @@
 (* 32 vs 61, using safe_tac with imp in asm would be unfortunate (5steps) *)
 
 lemma eps1_aux1:
-    "[|m le n; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|] 
+    "[|m \<le> n; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
      ==> rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)"
 apply (erule rev_mp) (* For induction proof *)
 apply (induct_tac n)
@@ -1823,16 +1823,16 @@
 apply (rule_tac [2] e_less_le [THEN ssubst])
 apply (assumption | rule emb_chain_cpo nat_succI)+
 apply (subst comp_fun_apply)
-apply (assumption | 
-       rule emb_chain_emb [THEN emb_cont]  e_less_cont cont_fun apply_type 
+apply (assumption |
+       rule emb_chain_emb [THEN emb_cont]  e_less_cont cont_fun apply_type
             Dinf_prod)+
 apply (rule_tac y = "x`xa" in emb_chain_emb [THEN emb_cont, THEN cont_mono])
 apply (assumption | rule e_less_cont [THEN cont_fun]  apply_type Dinf_prod)+
 apply (rule_tac x1 = x and n1 = xa in Dinf_eq [THEN subst])
 apply (rule_tac [3] comp_fun_apply [THEN subst])
 apply (rename_tac [5] y)
-apply (rule_tac [5] P = 
-         "%z. rel(DD`succ(y), 
+apply (rule_tac [5] P =
+         "%z. rel(DD`succ(y),
                   (ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
                   z)"
        in id_conv [THEN subst])
@@ -1851,7 +1851,7 @@
 (* 18 vs 40 *)
 
 lemma eps1_aux2:
-    "[|n le m; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|] 
+    "[|n \<le> m; emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
      ==> rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)"
 apply (erule rev_mp) (* For induction proof *)
 apply (induct_tac m)
@@ -1866,8 +1866,8 @@
 apply (subst e_gr_le)
 apply (rule_tac [4] comp_fun_apply [THEN ssubst])
 apply (rule_tac [6] Dinf_eq [THEN ssubst])
-apply (assumption | 
-       rule emb_chain_emb emb_chain_cpo Rp_cont e_gr_cont cont_fun emb_cont 
+apply (assumption |
+       rule emb_chain_emb emb_chain_cpo Rp_cont e_gr_cont cont_fun emb_cont
             apply_type Dinf_prod nat_succI)+
 apply (simp add: e_gr_eq)
 apply (subst id_conv)
@@ -1875,7 +1875,7 @@
 done
 
 lemma eps1:
-    "[|emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|] 
+    "[|emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)); m \<in> nat; n \<in> nat|]
      ==> rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)"
 apply (simp add: eps_def)
 apply (blast intro: eps1_aux1 not_le_iff_lt [THEN iffD1, THEN leI, THEN eps1_aux2]
@@ -1887,7 +1887,7 @@
    Look for occurences of rel_cfI, rel_DinfI, etc to evaluate the problem. *)
 
 lemma lam_Dinf_cont:
-  "[| emb_chain(DD,ee); n \<in> nat |] 
+  "[| emb_chain(DD,ee); n \<in> nat |]
      ==> (\<lambda>x \<in> set(Dinf(DD,ee)). x`n) \<in> cont(Dinf(DD,ee),DD`n)"
 apply (rule contI)
 apply (assumption | rule lam_type apply_type Dinf_prod)+
@@ -1899,7 +1899,7 @@
 done
 
 lemma rho_projpair:
-    "[| emb_chain(DD,ee); n \<in> nat |] 
+    "[| emb_chain(DD,ee); n \<in> nat |]
      ==> projpair(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n),rho_proj(DD,ee,n))"
 apply (simp add: rho_proj_def)
 apply (rule projpairI)
@@ -1913,23 +1913,23 @@
 apply (rule_tac [4] comp_fun_apply [THEN ssubst])
 apply (rule_tac [6] beta [THEN ssubst])
 apply (rule_tac [7] rho_emb_id [THEN ssubst])
-apply (assumption | 
+apply (assumption |
        rule comp_fun id_type lam_type rho_emb_fun Dinf_prod [THEN apply_type]
             apply_type refl)+
 (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
-apply (rule rel_cfI) (* ------------------>>>Yields type cond, not in HOL *)
+apply (rule rel_cfI) (* ----------------\<longrightarrow>>>Yields type cond, not in HOL *)
 apply (subst id_conv)
 apply (rule_tac [2] comp_fun_apply [THEN ssubst])
 apply (rule_tac [4] beta [THEN ssubst])
 apply (rule_tac [5] rho_emb_apply1 [THEN ssubst])
-apply (rule_tac [6] rel_DinfI) 
+apply (rule_tac [6] rel_DinfI)
 apply (rule_tac [6] beta [THEN ssubst])
 (* Dinf_prod bad with lam_type *)
 apply (assumption |
        rule eps1 lam_type rho_emb_fun eps_fun
             Dinf_prod [THEN apply_type] refl)+
-apply (assumption | 
-       rule apply_type eps_fun Dinf_prod comp_pres_cont rho_emb_cont 
+apply (assumption |
+       rule apply_type eps_fun Dinf_prod comp_pres_cont rho_emb_cont
             lam_Dinf_cont id_cont cpo_Dinf emb_chain_cpo)+
 done
 
@@ -1937,7 +1937,7 @@
   "[| emb_chain(DD,ee); n \<in> nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))"
 by (auto simp add: emb_def intro: exI rho_projpair)
 
-lemma rho_proj_cont: "[| emb_chain(DD,ee); n \<in> nat |] 
+lemma rho_proj_cont: "[| emb_chain(DD,ee); n \<in> nat |]
      ==> rho_proj(DD,ee,n) \<in> cont(Dinf(DD,ee),DD`n)"
 by (auto intro: rho_projpair projpair_p_cont)
 
@@ -1947,7 +1947,7 @@
 
 lemma commuteI:
   "[| !!n. n \<in> nat ==> emb(DD`n,E,r(n));
-      !!m n. [|m le n; m \<in> nat; n \<in> nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |] 
+      !!m n. [|m \<le> n; m \<in> nat; n \<in> nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |]
      ==> commute(DD,ee,E,r)"
 by (simp add: commute_def)
 
@@ -1956,7 +1956,7 @@
 by (simp add: commute_def)
 
 lemma commute_eq:
-  "[| commute(DD,ee,E,r); m le n; m \<in> nat; n \<in> nat |] 
+  "[| commute(DD,ee,E,r); m \<le> n; m \<in> nat; n \<in> nat |]
      ==> r(n) O eps(DD,ee,m,n) = r(m) "
 by (simp add: commute_def)
 
@@ -1976,17 +1976,17 @@
 apply (auto intro: eps_fun)
 done
 
-lemma le_succ: "n \<in> nat ==> n le succ(n)"
+lemma le_succ: "n \<in> nat ==> n \<le> succ(n)"
 by (simp add: le_succ_iff)
 
 (* Shorter proof: 21 vs 83 (106 - 23, due to OAssoc complication) *)
 
 lemma commute_chain:
-    "[| commute(DD,ee,E,r); emb_chain(DD,ee); cpo(E) |] 
+    "[| commute(DD,ee,E,r); emb_chain(DD,ee); cpo(E) |]
      ==> chain(cf(E,E),\<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n)))"
 apply (rule chainI)
-apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont 
-                    emb_cont emb_chain_cpo, 
+apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
+                    emb_cont emb_chain_cpo,
        simp)
 apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
 apply (assumption | rule le_succ nat_succI)+
@@ -1995,14 +1995,14 @@
 apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *)
 apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst])
 apply (rule comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont 
+apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
                     emb_cont emb_chain_cpo le_succ)+
 apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
 apply (rule_tac [2] comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb 
+apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
                     Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
 apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
-apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf 
+apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
                     emb_chain_cpo embRp_rel emb_eps le_succ)+
 done
 
@@ -2013,14 +2013,14 @@
 by (auto intro: commute_chain rho_emb_commute cpo_Dinf)
 
 lemma rho_emb_chain_apply1:
-     "[| emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)) |] 
+     "[| emb_chain(DD,ee); x \<in> set(Dinf(DD,ee)) |]
       ==> chain(Dinf(DD,ee),
                 \<lambda>n \<in> nat.
                  (rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))`x)"
 by (drule rho_emb_chain [THEN chain_cf], assumption, simp)
 
 lemma chain_iprod_emb_chain:
-     "[| chain(iprod(DD),X); emb_chain(DD,ee); n \<in> nat |] 
+     "[| chain(iprod(DD),X); emb_chain(DD,ee); n \<in> nat |]
       ==> chain(DD`n,\<lambda>m \<in> nat. X `m `n)"
 by (auto intro: chain_iprod emb_chain_cpo)
 
@@ -2031,7 +2031,7 @@
      \<lambda>xa \<in> nat.
       (rho_emb(DD, ee, xa) O Rp(DD ` xa, Dinf(DD, ee),rho_emb(DD, ee, xa))) `
        x ` n)"
-by (frule rho_emb_chain_apply1 [THEN chain_Dinf, THEN chain_iprod_emb_chain], 
+by (frule rho_emb_chain_apply1 [THEN chain_Dinf, THEN chain_iprod_emb_chain],
     auto)
 
 (* Shorter proof: 32 vs 72 (roughly), Isabelle proof has lemmas. *)
@@ -2045,7 +2045,7 @@
 apply (rule cpo_cf) (*Instantiate variable, continued below (loops otherwise)*)
 apply (assumption | rule cpo_Dinf)+
 apply (rule islub_least)
-apply (assumption | 
+apply (assumption |
        rule cpo_lub rho_emb_chain cpo_cf cpo_Dinf isubI cont_cf id_cont)+
 apply simp
 apply (assumption | rule embRp_rel emb_rho_emb emb_chain_cpo cpo_Dinf)+
@@ -2055,7 +2055,7 @@
 apply (subst lub_Dinf)
 apply (assumption | rule rho_emb_chain_apply1)+
 defer 1
-apply (assumption | 
+apply (assumption |
        rule Dinf_prod cpo_lub [THEN islub_in]  id_cont cpo_Dinf cpo_cf cf_cont
             rho_emb_chain rho_emb_chain_apply1 id_cont [THEN cont_cf])+
 apply simp
@@ -2064,11 +2064,11 @@
 apply (rule_tac [6] x1 = "x`n" in chain_const [THEN chain_fun])
 defer 1
 apply (assumption |
-       rule rho_emb_chain_apply2 emb_chain_cpo islub_const apply_type 
+       rule rho_emb_chain_apply2 emb_chain_cpo islub_const apply_type
             Dinf_prod emb_chain_cpo chain_fun rho_emb_chain_apply2)+
 apply (rule dominateI, assumption, simp)
 apply (subst comp_fun_apply)
-apply (assumption | 
+apply (assumption |
        rule cont_fun Rp_cont emb_cont emb_rho_emb cpo_Dinf emb_chain_cpo)+
 apply (subst rho_projpair [THEN Rp_unique])
 prefer 5
@@ -2079,28 +2079,28 @@
 
 lemma theta_chain: (* almost same proof as commute_chain *)
     "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
-        emb_chain(DD,ee); cpo(E); cpo(G) |] 
+        emb_chain(DD,ee); cpo(E); cpo(G) |]
      ==> chain(cf(E,G),\<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n)))"
 apply (rule chainI)
-apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont 
-                    emb_cont emb_chain_cpo, 
+apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
+                    emb_cont emb_chain_cpo,
        simp)
 apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
 apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst])
 apply (assumption | rule le_succ nat_succI)+
 apply (subst Rp_comp)
 apply (assumption | rule emb_eps commute_emb emb_chain_cpo le_succ nat_succI)+
-apply (rule comp_assoc [THEN subst]) 
+apply (rule comp_assoc [THEN subst])
 apply (rule_tac r1 = "f (succ (n))" in comp_assoc [THEN ssubst])
 apply (rule comp_mono)
 apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
                      emb_cont emb_chain_cpo le_succ)+
 apply (rule_tac b="f(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
 apply (rule_tac [2] comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb 
+apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
                     Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
 apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
-apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf 
+apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
                     emb_chain_cpo embRp_rel emb_eps le_succ)+
 done
 
@@ -2109,7 +2109,7 @@
       emb_chain(DD,ee); cpo(E); cpo(G) |]
      ==> chain(cf(G,E),\<lambda>n \<in> nat. r(n) O Rp(DD`n,G,f(n)))"
 apply (rule chainI)
-apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont 
+apply (blast intro: lam_type cont_cf comp_pres_cont commute_emb Rp_cont
                     emb_cont emb_chain_cpo, simp)
 apply (rule_tac r1 = r and m1 = n in commute_eq [THEN subst])
 apply (rule_tac [5] r1 = f and m1 = n in commute_eq [THEN subst])
@@ -2119,14 +2119,14 @@
 apply (rule comp_assoc [THEN subst]) (* comp_assoc is simpler in Isa *)
 apply (rule_tac r1 = "r (succ (n))" in comp_assoc [THEN ssubst])
 apply (rule comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont 
+apply (blast intro: comp_pres_cont eps_cont emb_eps commute_emb Rp_cont
                     emb_cont emb_chain_cpo le_succ)+
 apply (rule_tac b="r(succ(n))" in comp_id [THEN subst]) (* 1 subst too much *)
 apply (rule_tac [2] comp_mono)
-apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb 
+apply (blast intro: comp_pres_cont eps_cont emb_eps emb_id commute_emb
                     Rp_cont emb_cont cont_fun emb_chain_cpo le_succ)+
 apply (subst comp_id) (* Undoes "1 subst too much", typing next anyway *)
-apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf 
+apply (blast intro: cont_fun Rp_cont emb_cont commute_emb cont_cf cpo_cf
                     emb_chain_cpo embRp_rel emb_eps le_succ)+
 done
 
@@ -2139,7 +2139,7 @@
 
 lemma commute_O_lemma:
      "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
-         emb_chain(DD,ee); cpo(E); cpo(G); x \<in> nat |] 
+         emb_chain(DD,ee); cpo(E); cpo(G); x \<in> nat |]
       ==> r(x) O Rp(DD ` x, G, f(x)) O f(x) O Rp(DD ` x, E, r(x)) =
           r(x) O Rp(DD ` x, E, r(x))"
 apply (rule_tac s1 = "f (x) " in comp_assoc [THEN subst])
@@ -2162,12 +2162,12 @@
 apply (simp add: projpair_def rho_proj_def, safe)
 apply (rule_tac [3] comp_lubs [THEN ssubst])
 (* The following one line is 15 lines in HOL, and includes existentials. *)
-apply (assumption | 
+apply (assumption |
        rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+
 apply (simp (no_asm) add: comp_assoc)
 apply (simp add: commute_O_lemma)
 apply (subst comp_lubs)
-apply (assumption | 
+apply (assumption |
        rule cf_cont islub_in cpo_lub cpo_cf theta_chain theta_proj_chain)+
 apply (simp (no_asm) add: comp_assoc)
 apply (simp add: commute_O_lemma)
@@ -2184,14 +2184,14 @@
 lemma emb_theta:
     "[| lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
         commute(DD,ee,E,r); commute(DD,ee,G,f);
-        emb_chain(DD,ee); cpo(E); cpo(G) |] 
+        emb_chain(DD,ee); cpo(E); cpo(G) |]
      ==> emb(E,G,lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n))))"
 apply (simp add: emb_def)
 apply (blast intro: theta_projpair)
 done
 
 lemma mono_lemma:
-    "[| g \<in> cont(D,D'); cpo(D); cpo(D'); cpo(E) |] 
+    "[| g \<in> cont(D,D'); cpo(D); cpo(D'); cpo(E) |]
      ==> (\<lambda>f \<in> cont(D',E). f O g) \<in> mono(cf(D',E),cf(D,E))"
 apply (rule monoI)
 apply (simp add: set_def cf_def)
@@ -2207,31 +2207,31 @@
            ((\<lambda>n \<in> nat. f(n) O Rp(DD ` n, E, r(n))) ` na))  =
           (\<lambda>na \<in> nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))"
 apply (rule fun_extension)
-(*something wrong here*) 
+(*something wrong here*)
 apply (auto simp del: beta_if simp add: beta intro: lam_type)
 done
 
 lemma chain_lemma:
      "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
-         emb_chain(DD,ee); cpo(E); cpo(G); n \<in> nat |] 
+         emb_chain(DD,ee); cpo(E); cpo(G); n \<in> nat |]
       ==> chain(cf(DD`n,G),\<lambda>x \<in> nat. (f(x) O Rp(DD ` x, E, r(x))) O r(n))"
 apply (rule commute_lam_lemma [THEN subst])
-apply (blast intro: theta_chain emb_chain_cpo 
+apply (blast intro: theta_chain emb_chain_cpo
                commute_emb [THEN emb_cont, THEN mono_lemma, THEN mono_chain])+
 done
 
 lemma suffix_lemma:
     "[| commute(DD,ee,E,r); commute(DD,ee,G,f);
-        emb_chain(DD,ee); cpo(E); cpo(G); cpo(DD`x); x \<in> nat |] 
-     ==> suffix(\<lambda>n \<in> nat. (f(n) O Rp(DD`n,E,r(n))) O r(x),x) = 
+        emb_chain(DD,ee); cpo(E); cpo(G); cpo(DD`x); x \<in> nat |]
+     ==> suffix(\<lambda>n \<in> nat. (f(n) O Rp(DD`n,E,r(n))) O r(x),x) =
          (\<lambda>n \<in> nat. f(x))"
 apply (simp add: suffix_def)
 apply (rule lam_type [THEN fun_extension])
-apply (blast intro: lam_type comp_fun cont_fun Rp_cont emb_cont 
+apply (blast intro: lam_type comp_fun cont_fun Rp_cont emb_cont
                     commute_emb emb_chain_cpo)+
 apply simp
 apply (rename_tac y)
-apply (subgoal_tac 
+apply (subgoal_tac
        "f(x#+y) O (Rp(DD`(x#+y), E, r(x#+y)) O r (x#+y)) O eps(DD, ee, x, x#+y)
         = f(x)")
 apply (simp add: comp_assoc commute_eq add_le_self)
@@ -2258,12 +2258,12 @@
 apply (assumption | rule mediatingI emb_theta)+
 apply (rule_tac b = "r (n) " in lub_const [THEN subst])
 apply (rule_tac [3] comp_lubs [THEN ssubst])
-apply (blast intro: cont_cf emb_cont commute_emb cpo_cf theta_chain 
+apply (blast intro: cont_cf emb_cont commute_emb cpo_cf theta_chain
                     chain_const emb_chain_cpo)+
 apply (simp (no_asm))
 apply (rule_tac n1 = n in lub_suffix [THEN subst])
 apply (assumption | rule chain_lemma cpo_cf emb_chain_cpo)+
-apply (simp add: suffix_lemma lub_const cont_cf emb_cont commute_emb cpo_cf 
+apply (simp add: suffix_lemma lub_const cont_cf emb_cont commute_emb cpo_cf
                  emb_chain_cpo)
 done
 
@@ -2271,7 +2271,7 @@
     "[| mediating(E,G,r,f,t);
         lub(cf(E,E), \<lambda>n \<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));
         commute(DD,ee,E,r); commute(DD,ee,G,f);
-        emb_chain(DD,ee); cpo(E); cpo(G) |] 
+        emb_chain(DD,ee); cpo(E); cpo(G) |]
      ==> t = lub(cf(E,G), \<lambda>n \<in> nat. f(n) O Rp(DD`n,E,r(n)))"
 apply (rule_tac b = t in comp_id [THEN subst])
 apply (erule_tac [2] subst)
@@ -2294,11 +2294,11 @@
     (Dinf(DD,ee),G,rho_emb(DD,ee),f,
      lub(cf(Dinf(DD,ee),G),
          \<lambda>n \<in> nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))) &
-   (\<forall>t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) -->
+   (\<forall>t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) \<longrightarrow>
      t = lub(cf(Dinf(DD,ee),G),
          \<lambda>n \<in> nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))))"
 apply safe
-apply (assumption | 
+apply (assumption |
        rule lub_universal_mediating rho_emb_commute rho_emb_lub cpo_Dinf)+
 apply (auto intro: lub_universal_unique rho_emb_commute rho_emb_lub cpo_Dinf)
 done
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/Primes.thy
--- a/src/ZF/ex/Primes.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Primes.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -14,7 +14,7 @@
 definition
   is_gcd  :: "[i,i,i]=>o"     --{*definition of great common divisor*}  where
     "is_gcd(p,m,n) == ((p dvd m) & (p dvd n))   &
-                       (\<forall>d\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
+                       (\<forall>d\<in>nat. (d dvd m) & (d dvd n) \<longrightarrow> d dvd p)"
 
 definition
   gcd     :: "[i,i]=>i"       --{*Euclid's algorithm for the gcd*}  where
@@ -28,7 +28,7 @@
   
 definition
   prime   :: i                --{*the set of prime numbers*}  where
-   "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p --> m=1 | m=p)}"
+   "prime == {p \<in> nat. 1<p & (\<forall>m \<in> nat. m dvd p \<longrightarrow> m=1 | m=p)}"
 
 
 subsection{*The Divides Relation*}
@@ -143,7 +143,7 @@
 (*Imitating TFL*)
 lemma gcd_induct_lemma [rule_format (no_asm)]: "[| n \<in> nat;  
          \<forall>m \<in> nat. P(m,0);  
-         \<forall>m \<in> nat. \<forall>n \<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |]  
+         \<forall>m \<in> nat. \<forall>n \<in> nat. 0<n \<longrightarrow> P(n, m mod n) \<longrightarrow> P(m,n) |]  
       ==> \<forall>m \<in> nat. P (m,n)"
 apply (erule_tac i = n in complete_induct)
 apply (case_tac "x=0")
@@ -206,7 +206,7 @@
 
 lemma gcd_greatest_raw [rule_format]:
      "[| m \<in> nat; n \<in> nat; f \<in> nat |]    
-      ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
+      ==> (f dvd m) \<longrightarrow> (f dvd n) \<longrightarrow> f dvd gcd(m,n)"
 apply (rule_tac m = m and n = n in gcd_induct)
 apply (simp_all add: gcd_non_0 dvd_mod)
 done
@@ -217,7 +217,7 @@
 done
 
 lemma gcd_greatest_iff [simp]: "[| k \<in> nat; m \<in> nat; n \<in> nat |]  
-      ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)"
+      ==> (k dvd gcd (m, n)) \<longleftrightarrow> (k dvd m & k dvd n)"
 by (blast intro!: gcd_greatest gcd_dvd1 gcd_dvd2 intro: dvd_trans)
 
 
@@ -235,7 +235,7 @@
 apply (blast intro: dvd_anti_sym)
 done
 
-lemma is_gcd_commute: "is_gcd(k,m,n) <-> is_gcd(k,n,m)"
+lemma is_gcd_commute: "is_gcd(k,m,n) \<longleftrightarrow> is_gcd(k,n,m)"
 by (simp add: is_gcd_def, blast)
 
 lemma gcd_commute_raw: "[| m \<in> nat; n \<in> nat |] ==> gcd(m,n) = gcd(n,m)"
@@ -331,7 +331,7 @@
 done
 
 lemma relprime_dvd_mult_iff:
-     "[| gcd (k,n) = 1;  m \<in> nat |] ==> k dvd (m #* n) <-> k dvd m"
+     "[| gcd (k,n) = 1;  m \<in> nat |] ==> k dvd (m #* n) \<longleftrightarrow> k dvd m"
 by (blast intro: dvdI2 relprime_dvd_mult dvd_trans)
 
 lemma prime_imp_relprime: 
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Ramsey.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -28,7 +28,7 @@
 
 definition
   Symmetric :: "i=>o" where
-    "Symmetric(E) == (\<forall>x y. <x,y>:E --> <y,x>:E)"
+    "Symmetric(E) == (\<forall>x y. <x,y>:E \<longrightarrow> <y,x>:E)"
 
 definition
   Atleast :: "[i,i]=>o" where -- "not really necessary: ZF defines cardinality"
@@ -36,15 +36,15 @@
 
 definition
   Clique  :: "[i,i,i]=>o" where
-    "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y --> <x,y> \<in> E)"
+    "Clique(C,V,E) == (C \<subseteq> V) & (\<forall>x \<in> C. \<forall>y \<in> C. x\<noteq>y \<longrightarrow> <x,y> \<in> E)"
 
 definition
   Indept  :: "[i,i,i]=>o" where
-    "Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y --> <x,y> \<notin> E)"
+    "Indept(I,V,E) == (I \<subseteq> V) & (\<forall>x \<in> I. \<forall>y \<in> I. x\<noteq>y \<longrightarrow> <x,y> \<notin> E)"
   
 definition
   Ramsey  :: "[i,i,i]=>o" where
-    "Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) -->  
+    "Ramsey(n,i,j) == \<forall>V E. Symmetric(E) & Atleast(n,V) \<longrightarrow>  
          (\<exists>C. Clique(C,V,E) & Atleast(i,C)) |       
          (\<exists>I. Indept(I,V,E) & Atleast(j,I))"
 
@@ -93,7 +93,7 @@
   the same proof could be used!!*)
 lemma pigeon2 [rule_format]:
      "m \<in> nat ==>  
-          \<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A Un B) -->    
+          \<forall>n \<in> nat. \<forall>A B. Atleast((m#+n) #- succ(0), A \<union> B) \<longrightarrow>    
                            Atleast(m,A) | Atleast(n,B)"
 apply (induct_tac "m")
 apply (blast intro!: Atleast0, simp)
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/Ring.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -115,13 +115,13 @@
 
 lemma (in abelian_group) a_l_cancel [simp]:
      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
-      \<Longrightarrow> (x \<oplus> y = x \<oplus> z) <-> (y = z)"
+      \<Longrightarrow> (x \<oplus> y = x \<oplus> z) \<longleftrightarrow> (y = z)"
 by (rule group.l_cancel [OF a_group,
              simplified, simplified ring_add_def [symmetric]])
 
 lemma (in abelian_group) a_r_cancel [simp]:
      "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G); z \<in> carrier(G)\<rbrakk>
-      \<Longrightarrow> (y \<oplus> x = z \<oplus> x) <-> (y = z)"
+      \<Longrightarrow> (y \<oplus> x = z \<oplus> x) \<longleftrightarrow> (y = z)"
 by (rule group.r_cancel [OF a_group, simplified, simplified ring_add_def [symmetric]])
 
 lemma (in abelian_monoid) a_assoc:
@@ -234,7 +234,7 @@
   ring_hom :: "[i,i] => i" where
   "ring_hom(R,S) ==
     {h \<in> carrier(R) -> carrier(S).
-      (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
+      (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) \<longrightarrow>
         h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
         h ` (x \<oplus>\<^bsub>R\<^esub> y) = (h ` x) \<oplus>\<^bsub>S\<^esub> (h ` y)) &
       h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
diff -r ff6b0c1087f2 -r 95f1e700b712 src/ZF/ex/misc.thy
--- a/src/ZF/ex/misc.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/ex/misc.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -31,16 +31,16 @@
 
 
 text{*A weird property of ordered pairs.*}
-lemma "b\<noteq>c ==> <a,b> Int <a,c> = <a,a>"
+lemma "b\<noteq>c ==> <a,b> \<inter> <a,c> = <a,a>"
 by (simp add: Pair_def Int_cons_left Int_cons_right doubleton_eq_iff, blast)
 
 text{*These two are cited in Benzmueller and Kohlhase's system description of
  LEO, CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*}
-lemma "(X = Y Un Z) <-> (Y \<subseteq> X & Z \<subseteq> X & (\<forall>V. Y \<subseteq> V & Z \<subseteq> V --> X \<subseteq> V))"
+lemma "(X = Y \<union> Z) \<longleftrightarrow> (Y \<subseteq> X & Z \<subseteq> X & (\<forall>V. Y \<subseteq> V & Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
 by (blast intro!: equalityI)
 
 text{*the dual of the previous one*}
-lemma "(X = Y Int Z) <-> (X \<subseteq> Y & X \<subseteq> Z & (\<forall>V. V \<subseteq> Y & V \<subseteq> Z --> V \<subseteq> X))"
+lemma "(X = Y \<inter> Z) \<longleftrightarrow> (X \<subseteq> Y & X \<subseteq> Z & (\<forall>V. V \<subseteq> Y & V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
 by (blast intro!: equalityI)
 
 text{*trivial example of term synthesis: apparently hard for some provers!*}
@@ -52,18 +52,18 @@
 by blast
 
 text{*variant of the benchmark above*}
-lemma "\<forall>x \<in> S. Union(S) \<subseteq> x ==> \<exists>z. S \<subseteq> {z}"
+lemma "\<forall>x \<in> S. \<Union>(S) \<subseteq> x ==> \<exists>z. S \<subseteq> {z}"
 by blast
 
 (*Example 12 (credited to Peter Andrews) from
  W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
  In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
  Ellis Horwood, 53-100 (1979). *)
-lemma "(\<forall>F. {x} \<in> F --> {y} \<in> F) --> (\<forall>A. x \<in> A --> y \<in> A)"
+lemma "(\<forall>F. {x} \<in> F \<longrightarrow> {y} \<in> F) \<longrightarrow> (\<forall>A. x \<in> A \<longrightarrow> y \<in> A)"
 by best
 
 text{*A characterization of functions suggested by Tobias Nipkow*}
-lemma "r \<in> domain(r)->B  <->  r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> X)"
+lemma "r \<in> domain(r)->B  \<longleftrightarrow>  r \<subseteq> domain(r)*B & (\<forall>X. r `` (r -`` X) \<subseteq> X)"
 by (unfold Pi_def function_def, best)
 
 
@@ -81,8 +81,8 @@
   rewriting does not instantiate Vars.*)
 lemma "(\<forall>A f B g. hom(A,f,B,g) =  
            {H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &  
-                     (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) -->  
-       J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) -->   
+                     (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) \<longrightarrow>  
+       J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) \<longrightarrow>   
        (K O J) \<in> hom(A,f,C,h)"
 by force
 
@@ -90,7 +90,7 @@
 lemma "(!! A f B g. hom(A,f,B,g) ==  
            {H \<in> A->B. f \<in> A*A->A & g \<in> B*B->B &  
                      (\<forall>x \<in> A. \<forall>y \<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) 
-       ==> J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) --> (K O J) \<in> hom(A,f,C,h)"
+       ==> J \<in> hom(A,f,B,g) & K \<in> hom(B,g,C,h) \<longrightarrow> (K O J) \<in> hom(A,f,C,h)"
 by force