diff -r f2094906e491 -r e44d86131648 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Cardinal.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -10,31 +10,31 @@
 definition
   (*least ordinal operator*)
    Least    :: "(i=>o) => i"    (binder \<open>\<mu> \<close> 10)  where
-     "Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))"
+     "Least(P) \<equiv> THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> \<not>P(j))"
 
 definition
   eqpoll   :: "[i,i] => o"     (infixl \<open>\<approx>\<close> 50)  where
-    "A \<approx> B == \<exists>f. f \<in> bij(A,B)"
+    "A \<approx> B \<equiv> \<exists>f. f \<in> bij(A,B)"
 
 definition
   lepoll   :: "[i,i] => o"     (infixl \<open>\<lesssim>\<close> 50)  where
-    "A \<lesssim> B == \<exists>f. f \<in> inj(A,B)"
+    "A \<lesssim> B \<equiv> \<exists>f. f \<in> inj(A,B)"
 
 definition
   lesspoll :: "[i,i] => o"     (infixl \<open>\<prec>\<close> 50)  where
-    "A \<prec> B == A \<lesssim> B & ~(A \<approx> B)"
+    "A \<prec> B \<equiv> A \<lesssim> B & \<not>(A \<approx> B)"
 
 definition
   cardinal :: "i=>i"           (\<open>|_|\<close>)  where
-    "|A| == (\<mu> i. i \<approx> A)"
+    "|A| \<equiv> (\<mu> i. i \<approx> A)"
 
 definition
   Finite   :: "i=>o"  where
-    "Finite(A) == \<exists>n\<in>nat. A \<approx> n"
+    "Finite(A) \<equiv> \<exists>n\<in>nat. A \<approx> n"
 
 definition
   Card     :: "i=>o"  where
-    "Card(i) == (i = |i|)"
+    "Card(i) \<equiv> (i = |i|)"
 
 
 subsection\<open>The Schroeder-Bernstein Theorem\<close>
@@ -47,7 +47,7 @@
 
 lemma Banach_last_equation:
     "g \<in> Y->X
-     ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
+     \<Longrightarrow> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
          X - lfp(X, %W. X - g``(Y - f``W))"
 apply (rule_tac P = "%u. v = X-u" for v
        in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
@@ -55,7 +55,7 @@
 done
 
 lemma decomposition:
-     "[| f \<in> X->Y;  g \<in> Y->X |] ==>
+     "\<lbrakk>f \<in> X->Y;  g \<in> Y->X\<rbrakk> \<Longrightarrow>
       \<exists>XA XB YA YB. (XA \<inter> XB = 0) & (XA \<union> XB = X) &
                       (YA \<inter> YB = 0) & (YA \<union> YB = Y) &
                       f``XA=YA & g``YB=XB"
@@ -67,18 +67,18 @@
 done
 
 lemma schroeder_bernstein:
-    "[| f \<in> inj(X,Y);  g \<in> inj(Y,X) |] ==> \<exists>h. h \<in> bij(X,Y)"
+    "\<lbrakk>f \<in> inj(X,Y);  g \<in> inj(Y,X)\<rbrakk> \<Longrightarrow> \<exists>h. h \<in> bij(X,Y)"
 apply (insert decomposition [of f X Y g])
 apply (simp add: inj_is_fun)
 apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
 (* The instantiation of exI to @{term"restrict(f,XA) \<union> converse(restrict(g,YB))"}
-   is forced by the context!! *)
+   is forced by the context\<And>*)
 done
 
 
 (** Equipollence is an equivalence relation **)
 
-lemma bij_imp_eqpoll: "f \<in> bij(A,B) ==> A \<approx> B"
+lemma bij_imp_eqpoll: "f \<in> bij(A,B) \<Longrightarrow> A \<approx> B"
 apply (unfold eqpoll_def)
 apply (erule exI)
 done
@@ -86,20 +86,20 @@
 (*A \<approx> A*)
 lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
 
-lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
+lemma eqpoll_sym: "X \<approx> Y \<Longrightarrow> Y \<approx> X"
 apply (unfold eqpoll_def)
 apply (blast intro: bij_converse_bij)
 done
 
 lemma eqpoll_trans [trans]:
-    "[| X \<approx> Y;  Y \<approx> Z |] ==> X \<approx> Z"
+    "\<lbrakk>X \<approx> Y;  Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<approx> Z"
 apply (unfold eqpoll_def)
 apply (blast intro: comp_bij)
 done
 
 (** Le-pollence is a partial ordering **)
 
-lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y"
+lemma subset_imp_lepoll: "X<=Y \<Longrightarrow> X \<lesssim> Y"
 apply (unfold lepoll_def)
 apply (rule exI)
 apply (erule id_subset_inj)
@@ -109,35 +109,35 @@
 
 lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
 
-lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
+lemma eqpoll_imp_lepoll: "X \<approx> Y \<Longrightarrow> X \<lesssim> Y"
 by (unfold eqpoll_def bij_def lepoll_def, blast)
 
-lemma lepoll_trans [trans]: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
+lemma lepoll_trans [trans]: "\<lbrakk>X \<lesssim> Y;  Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<lesssim> Z"
 apply (unfold lepoll_def)
 apply (blast intro: comp_inj)
 done
 
-lemma eq_lepoll_trans [trans]: "[| X \<approx> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
+lemma eq_lepoll_trans [trans]: "\<lbrakk>X \<approx> Y;  Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<lesssim> Z"
  by (blast intro: eqpoll_imp_lepoll lepoll_trans)
 
-lemma lepoll_eq_trans [trans]: "[| X \<lesssim> Y;  Y \<approx> Z |] ==> X \<lesssim> Z"
+lemma lepoll_eq_trans [trans]: "\<lbrakk>X \<lesssim> Y;  Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<lesssim> Z"
  by (blast intro: eqpoll_imp_lepoll lepoll_trans)
 
 (*Asymmetry law*)
-lemma eqpollI: "[| X \<lesssim> Y;  Y \<lesssim> X |] ==> X \<approx> Y"
+lemma eqpollI: "\<lbrakk>X \<lesssim> Y;  Y \<lesssim> X\<rbrakk> \<Longrightarrow> X \<approx> Y"
 apply (unfold lepoll_def eqpoll_def)
 apply (elim exE)
 apply (rule schroeder_bernstein, assumption+)
 done
 
 lemma eqpollE:
-    "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
+    "\<lbrakk>X \<approx> Y; \<lbrakk>X \<lesssim> Y; Y \<lesssim> X\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
 by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
 
 lemma eqpoll_iff: "X \<approx> Y \<longleftrightarrow> X \<lesssim> Y & Y \<lesssim> X"
 by (blast intro: eqpollI elim!: eqpollE)
 
-lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
+lemma lepoll_0_is_0: "A \<lesssim> 0 \<Longrightarrow> A = 0"
 apply (unfold lepoll_def inj_def)
 apply (blast dest: apply_type)
 done
@@ -149,20 +149,20 @@
 by (blast intro: lepoll_0_is_0 lepoll_refl)
 
 lemma Un_lepoll_Un:
-    "[| A \<lesssim> B; C \<lesssim> D; B \<inter> D = 0 |] ==> A \<union> C \<lesssim> B \<union> D"
+    "\<lbrakk>A \<lesssim> B; C \<lesssim> D; B \<inter> D = 0\<rbrakk> \<Longrightarrow> A \<union> C \<lesssim> B \<union> D"
 apply (unfold lepoll_def)
 apply (blast intro: inj_disjoint_Un)
 done
 
-(*A \<approx> 0 ==> A=0*)
+(*A \<approx> 0 \<Longrightarrow> A=0*)
 lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
 
 lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
 by (blast intro: eqpoll_0_is_0 eqpoll_refl)
 
 lemma eqpoll_disjoint_Un:
-    "[| A \<approx> B;  C \<approx> D;  A \<inter> C = 0;  B \<inter> D = 0 |]
-     ==> A \<union> C \<approx> B \<union> D"
+    "\<lbrakk>A \<approx> B;  C \<approx> D;  A \<inter> C = 0;  B \<inter> D = 0\<rbrakk>
+     \<Longrightarrow> A \<union> C \<approx> B \<union> D"
 apply (unfold eqpoll_def)
 apply (blast intro: bij_disjoint_Un)
 done
@@ -170,16 +170,16 @@
 
 subsection\<open>lesspoll: contributions by Krzysztof Grabczewski\<close>
 
-lemma lesspoll_not_refl: "~ (i \<prec> i)"
+lemma lesspoll_not_refl: "\<not> (i \<prec> i)"
 by (simp add: lesspoll_def)
 
-lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P"
+lemma lesspoll_irrefl [elim!]: "i \<prec> i \<Longrightarrow> P"
 by (simp add: lesspoll_def)
 
-lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
+lemma lesspoll_imp_lepoll: "A \<prec> B \<Longrightarrow> A \<lesssim> B"
 by (unfold lesspoll_def, blast)
 
-lemma lepoll_well_ord: "[| A \<lesssim> B; well_ord(B,r) |] ==> \<exists>s. well_ord(A,s)"
+lemma lepoll_well_ord: "\<lbrakk>A \<lesssim> B; well_ord(B,r)\<rbrakk> \<Longrightarrow> \<exists>s. well_ord(A,s)"
 apply (unfold lepoll_def)
 apply (blast intro: well_ord_rvimage)
 done
@@ -207,36 +207,36 @@
 (** Variations on transitivity **)
 
 lemma lesspoll_trans [trans]:
-      "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
+      "\<lbrakk>X \<prec> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
 apply (unfold lesspoll_def)
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
 lemma lesspoll_trans1 [trans]:
-      "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
+      "\<lbrakk>X \<lesssim> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
 apply (unfold lesspoll_def)
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
 lemma lesspoll_trans2 [trans]:
-      "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
+      "\<lbrakk>X \<prec> Y; Y \<lesssim> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
 apply (unfold lesspoll_def)
 apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
 done
 
 lemma eq_lesspoll_trans [trans]:
-      "[| X \<approx> Y; Y \<prec> Z |] ==> X \<prec> Z"
+      "\<lbrakk>X \<approx> Y; Y \<prec> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
   by (blast intro: eqpoll_imp_lepoll lesspoll_trans1)
 
 lemma lesspoll_eq_trans [trans]:
-      "[| X \<prec> Y; Y \<approx> Z |] ==> X \<prec> Z"
+      "\<lbrakk>X \<prec> Y; Y \<approx> Z\<rbrakk> \<Longrightarrow> X \<prec> Z"
   by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)
 
 
 (** \<mu> -- the least number operator [from HOL/Univ.ML] **)
 
 lemma Least_equality:
-    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (\<mu> x. P(x)) = i"
+    "\<lbrakk>P(i);  Ord(i);  \<And>x. x<i \<Longrightarrow> \<not>P(x)\<rbrakk> \<Longrightarrow> (\<mu> x. P(x)) = i"
 apply (unfold Least_def)
 apply (rule the_equality, blast)
 apply (elim conjE)
@@ -254,7 +254,7 @@
             case True thus ?thesis .
           next
             case False
-            hence "\<And>x. x \<in> i \<Longrightarrow> ~P(x)" using step
+            hence "\<And>x. x \<in> i \<Longrightarrow> \<not>P(x)" using step
               by blast
             hence "(\<mu> a. P(a)) = i" using step
               by (blast intro: Least_equality ltD) 
@@ -278,7 +278,7 @@
             case True thus ?thesis .
           next
             case False
-            hence "\<And>x. x \<in> i \<Longrightarrow> ~ (\<mu> a. P(a)) \<le> i" using step
+            hence "\<And>x. x \<in> i \<Longrightarrow> \<not> (\<mu> a. P(a)) \<le> i" using step
               by blast
             hence "(\<mu> a. P(a)) = i" using step
               by (blast elim: ltE intro: ltI Least_equality lt_trans1)
@@ -291,19 +291,19 @@
 qed
 
 (*\<mu> really is the smallest*)
-lemma less_LeastE: "[| P(i);  i < (\<mu> x. P(x)) |] ==> Q"
+lemma less_LeastE: "\<lbrakk>P(i);  i < (\<mu> x. P(x))\<rbrakk> \<Longrightarrow> Q"
 apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
 apply (simp add: lt_Ord)
 done
 
 (*Easier to apply than LeastI: conclusion has only one occurrence of P*)
 lemma LeastI2:
-    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(\<mu> j. P(j))"
+    "\<lbrakk>P(i);  Ord(i);  \<And>j. P(j) \<Longrightarrow> Q(j)\<rbrakk> \<Longrightarrow> Q(\<mu> j. P(j))"
 by (blast intro: LeastI )
 
 (*If there is no such P then \<mu> is vacuously 0*)
 lemma Least_0:
-    "[| ~ (\<exists>i. Ord(i) & P(i)) |] ==> (\<mu> x. P(x)) = 0"
+    "\<lbrakk>\<not> (\<exists>i. Ord(i) & P(i))\<rbrakk> \<Longrightarrow> (\<mu> x. P(x)) = 0"
 apply (unfold Least_def)
 apply (rule the_0, blast)
 done
@@ -326,12 +326,12 @@
 subsection\<open>Basic Properties of Cardinals\<close>
 
 (*Not needed for simplification, but helpful below*)
-lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))"
+lemma Least_cong: "(\<And>y. P(y) \<longleftrightarrow> Q(y)) \<Longrightarrow> (\<mu> x. P(x)) = (\<mu> x. Q(x))"
 by simp
 
-(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"};  see well_ord_lepoll_imp_cardinal_le
+(*Need AC to get @{term"X \<lesssim> Y \<Longrightarrow> |X| \<le> |Y|"};  see well_ord_lepoll_imp_cardinal_le
   Converse also requires AC, but see well_ord_cardinal_eqE*)
-lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
+lemma cardinal_cong: "X \<approx> Y \<Longrightarrow> |X| = |Y|"
 apply (unfold eqpoll_def cardinal_def)
 apply (rule Least_cong)
 apply (blast intro: comp_bij bij_converse_bij)
@@ -345,7 +345,7 @@
     by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) 
 qed
 
-(* @{term"Ord(A) ==> |A| \<approx> A"} *)
+(* @{term"Ord(A) \<Longrightarrow> |A| \<approx> A"} *)
 lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
 
 lemma Ord_cardinal_idem: "Ord(A) \<Longrightarrow> ||A|| = |A|"
@@ -362,36 +362,36 @@
 qed
 
 lemma well_ord_cardinal_eqpoll_iff:
-     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
+     "\<lbrakk>well_ord(X,r);  well_ord(Y,s)\<rbrakk> \<Longrightarrow> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
 by (blast intro: cardinal_cong well_ord_cardinal_eqE)
 
 
 (** Observations from Kunen, page 28 **)
 
-lemma Ord_cardinal_le: "Ord(i) ==> |i| \<le> i"
+lemma Ord_cardinal_le: "Ord(i) \<Longrightarrow> |i| \<le> i"
 apply (unfold cardinal_def)
 apply (erule eqpoll_refl [THEN Least_le])
 done
 
-lemma Card_cardinal_eq: "Card(K) ==> |K| = K"
+lemma Card_cardinal_eq: "Card(K) \<Longrightarrow> |K| = K"
 apply (unfold Card_def)
 apply (erule sym)
 done
 
-(* Could replace the  @{term"~(j \<approx> i)"}  by  @{term"~(i \<preceq> j)"}. *)
-lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
+(* Could replace the  @{term"\<not>(j \<approx> i)"}  by  @{term"\<not>(i \<preceq> j)"}. *)
+lemma CardI: "\<lbrakk>Ord(i);  \<And>j. j<i \<Longrightarrow> \<not>(j \<approx> i)\<rbrakk> \<Longrightarrow> Card(i)"
 apply (unfold Card_def cardinal_def)
 apply (subst Least_equality)
 apply (blast intro: eqpoll_refl)+
 done
 
-lemma Card_is_Ord: "Card(i) ==> Ord(i)"
+lemma Card_is_Ord: "Card(i) \<Longrightarrow> Ord(i)"
 apply (unfold Card_def cardinal_def)
 apply (erule ssubst)
 apply (rule Ord_Least)
 done
 
-lemma Card_cardinal_le: "Card(K) ==> K \<le> |K|"
+lemma Card_cardinal_le: "Card(K) \<Longrightarrow> K \<le> |K|"
 apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
 done
 
@@ -401,7 +401,7 @@
 done
 
 text\<open>The cardinals are the initial ordinals.\<close>
-lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
+lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> \<not> j \<approx> K)"
 proof -
   { fix j
     assume K: "Card(K)" "j \<approx> K"
@@ -416,7 +416,7 @@
     by (blast intro: CardI Card_is_Ord) 
 qed
 
-lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
+lemma lt_Card_imp_lesspoll: "\<lbrakk>Card(a); i<a\<rbrakk> \<Longrightarrow> i \<prec> a"
 apply (unfold lesspoll_def)
 apply (drule Card_iff_initial [THEN iffD1])
 apply (blast intro!: leI [THEN le_imp_lepoll])
@@ -427,7 +427,7 @@
 apply (blast elim!: ltE)
 done
 
-lemma Card_Un: "[| Card(K);  Card(L) |] ==> Card(K \<union> L)"
+lemma Card_Un: "\<lbrakk>Card(K);  Card(L)\<rbrakk> \<Longrightarrow> Card(K \<union> L)"
 apply (rule Ord_linear_le [of K L])
 apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_is_Ord le_imp_subset
                      subset_Un_iff2 [THEN iffD1])
@@ -491,19 +491,19 @@
 qed
 
 text\<open>Since we have \<^term>\<open>|succ(nat)| \<le> |nat|\<close>, the converse of \<open>cardinal_mono\<close> fails!\<close>
-lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
+lemma cardinal_lt_imp_lt: "\<lbrakk>|i| < |j|;  Ord(i);  Ord(j)\<rbrakk> \<Longrightarrow> i < j"
 apply (rule Ord_linear2 [of i j], assumption+)
 apply (erule lt_trans2 [THEN lt_irrefl])
 apply (erule cardinal_mono)
 done
 
-lemma Card_lt_imp_lt: "[| |i| < K;  Ord(i);  Card(K) |] ==> i < K"
+lemma Card_lt_imp_lt: "\<lbrakk>|i| < K;  Ord(i);  Card(K)\<rbrakk> \<Longrightarrow> i < K"
   by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
 
-lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)"
+lemma Card_lt_iff: "\<lbrakk>Ord(i);  Card(K)\<rbrakk> \<Longrightarrow> (|i| < K) \<longleftrightarrow> (i < K)"
 by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
 
-lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)"
+lemma Card_le_iff: "\<lbrakk>Ord(i);  Card(K)\<rbrakk> \<Longrightarrow> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)"
 by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
 
 (*Can use AC or finiteness to discharge first premise*)
@@ -526,21 +526,21 @@
   thus ?thesis by simp
 qed
 
-lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
+lemma lepoll_cardinal_le: "\<lbrakk>A \<lesssim> i; Ord(i)\<rbrakk> \<Longrightarrow> |A| \<le> i"
 apply (rule le_trans)
 apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_cardinal_le], assumption)
 apply (erule Ord_cardinal_le)
 done
 
-lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
+lemma lepoll_Ord_imp_eqpoll: "\<lbrakk>A \<lesssim> i; Ord(i)\<rbrakk> \<Longrightarrow> |A| \<approx> A"
 by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
 
-lemma lesspoll_imp_eqpoll: "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
+lemma lesspoll_imp_eqpoll: "\<lbrakk>A \<prec> i; Ord(i)\<rbrakk> \<Longrightarrow> |A| \<approx> A"
 apply (unfold lesspoll_def)
 apply (blast intro: lepoll_Ord_imp_eqpoll)
 done
 
-lemma cardinal_subset_Ord: "[|A<=i; Ord(i)|] ==> |A| \<subseteq> i"
+lemma cardinal_subset_Ord: "\<lbrakk>A<=i; Ord(i)\<rbrakk> \<Longrightarrow> |A| \<subseteq> i"
 apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le])
 apply (auto simp add: lt_def)
 apply (blast intro: Ord_trans)
@@ -549,7 +549,7 @@
 subsection\<open>The finite cardinals\<close>
 
 lemma cons_lepoll_consD:
- "[| cons(u,A) \<lesssim> cons(v,B);  u\<notin>A;  v\<notin>B |] ==> A \<lesssim> B"
+ "\<lbrakk>cons(u,A) \<lesssim> cons(v,B);  u\<notin>A;  v\<notin>B\<rbrakk> \<Longrightarrow> A \<lesssim> B"
 apply (unfold lepoll_def inj_def, safe)
 apply (rule_tac x = "\<lambda>x\<in>A. if f`x=v then f`u else f`x" in exI)
 apply (rule CollectI)
@@ -562,13 +562,13 @@
 apply blast
 done
 
-lemma cons_eqpoll_consD: "[| cons(u,A) \<approx> cons(v,B);  u\<notin>A;  v\<notin>B |] ==> A \<approx> B"
+lemma cons_eqpoll_consD: "\<lbrakk>cons(u,A) \<approx> cons(v,B);  u\<notin>A;  v\<notin>B\<rbrakk> \<Longrightarrow> A \<approx> B"
 apply (simp add: eqpoll_iff)
 apply (blast intro: cons_lepoll_consD)
 done
 
 (*Lemma suggested by Mike Fourman*)
-lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n"
+lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) \<Longrightarrow> m \<lesssim> n"
 apply (unfold succ_def)
 apply (erule cons_lepoll_consD)
 apply (rule mem_not_refl)+
@@ -576,7 +576,7 @@
 
 
 lemma nat_lepoll_imp_le:
-     "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
+     "m \<in> nat \<Longrightarrow> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
 proof (induct m arbitrary: n rule: nat_induct)
   case 0 thus ?case by (blast intro!: nat_0_le)
 next
@@ -591,7 +591,7 @@
     qed
 qed
 
-lemma nat_eqpoll_iff: "[| m \<in> nat; n \<in> nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
+lemma nat_eqpoll_iff: "\<lbrakk>m \<in> nat; n \<in> nat\<rbrakk> \<Longrightarrow> m \<approx> n \<longleftrightarrow> m = n"
 apply (rule iffI)
 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
 apply (simp add: eqpoll_refl)
@@ -616,11 +616,11 @@
 
 
 (*Part of Kunen's Lemma 10.6*)
-lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n \<in> nat |] ==> P"
+lemma succ_lepoll_natE: "\<lbrakk>succ(n) \<lesssim> n;  n \<in> nat\<rbrakk> \<Longrightarrow> P"
 by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
 
 lemma nat_lepoll_imp_ex_eqpoll_n:
-     "[| n \<in> nat;  nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
+     "\<lbrakk>n \<in> nat;  nat \<lesssim> X\<rbrakk> \<Longrightarrow> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
 apply (unfold lepoll_def eqpoll_def)
 apply (fast del: subsetI subsetCE
             intro!: subset_SIs
@@ -649,22 +649,22 @@
 qed
 
 lemma lesspoll_succ_imp_lepoll:
-     "[| A \<prec> succ(m); m \<in> nat |] ==> A \<lesssim> m"
+     "\<lbrakk>A \<prec> succ(m); m \<in> nat\<rbrakk> \<Longrightarrow> A \<lesssim> m"
 apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def)
 apply (auto dest: inj_not_surj_succ)
 done
 
-lemma lesspoll_succ_iff: "m \<in> nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
+lemma lesspoll_succ_iff: "m \<in> nat \<Longrightarrow> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
 by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
 
-lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m \<in> nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
+lemma lepoll_succ_disj: "\<lbrakk>A \<lesssim> succ(m);  m \<in> nat\<rbrakk> \<Longrightarrow> A \<lesssim> m | A \<approx> succ(m)"
 apply (rule disjCI)
 apply (rule lesspoll_succ_imp_lepoll)
 prefer 2 apply assumption
 apply (simp (no_asm_simp) add: lesspoll_def)
 done
 
-lemma lesspoll_cardinal_lt: "[| A \<prec> i; Ord(i) |] ==> |A| < i"
+lemma lesspoll_cardinal_lt: "\<lbrakk>A \<prec> i; Ord(i)\<rbrakk> \<Longrightarrow> |A| < i"
 apply (unfold lesspoll_def, clarify)
 apply (frule lepoll_cardinal_le, assumption)
 apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
@@ -676,7 +676,7 @@
 
 (*This implies Kunen's Lemma 10.6*)
 lemma lt_not_lepoll:
-  assumes n: "n<i" "n \<in> nat" shows "~ i \<lesssim> n"
+  assumes n: "n<i" "n \<in> nat" shows "\<not> i \<lesssim> n"
 proof -
   { assume i: "i \<lesssim> n"
     have "succ(n) \<lesssim> i" using n
@@ -700,8 +700,8 @@
   thus ?thesis by (simp add: eqpoll_refl)
 next
   case gt
-  hence  "~ i \<lesssim> n" using n  by (rule lt_not_lepoll)
-  hence  "~ i \<approx> n" using n  by (blast intro: eqpoll_imp_lepoll)
+  hence  "\<not> i \<lesssim> n" using n  by (rule lt_not_lepoll)
+  hence  "\<not> i \<approx> n" using n  by (blast intro: eqpoll_imp_lepoll)
   moreover have "i \<noteq> n" using \<open>n<i\<close> by auto
   ultimately show ?thesis by blast
 qed
@@ -710,7 +710,7 @@
 proof -
   { fix i
     assume i: "i < nat" "i \<approx> nat"
-    hence "~ nat \<lesssim> i"
+    hence "\<not> nat \<lesssim> i"
       by (simp add: lt_def lt_not_lepoll)
     hence False using i
       by (simp add: eqpoll_iff)
@@ -721,12 +721,12 @@
 qed
 
 (*Allows showing that |i| is a limit cardinal*)
-lemma nat_le_cardinal: "nat \<le> i ==> nat \<le> |i|"
+lemma nat_le_cardinal: "nat \<le> i \<Longrightarrow> nat \<le> |i|"
 apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
 apply (erule cardinal_mono)
 done
 
-lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
+lemma n_lesspoll_nat: "n \<in> nat \<Longrightarrow> n \<prec> nat"
   by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)
 
 
@@ -735,7 +735,7 @@
 
 (*Congruence law for  cons  under equipollence*)
 lemma cons_lepoll_cong:
-    "[| A \<lesssim> B;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)"
+    "\<lbrakk>A \<lesssim> B;  b \<notin> B\<rbrakk> \<Longrightarrow> cons(a,A) \<lesssim> cons(b,B)"
 apply (unfold lepoll_def, safe)
 apply (rule_tac x = "\<lambda>y\<in>cons (a,A) . if y=a then b else f`y" in exI)
 apply (rule_tac d = "%z. if z \<in> B then converse (f) `z else a" in lam_injective)
@@ -745,15 +745,15 @@
 done
 
 lemma cons_eqpoll_cong:
-     "[| A \<approx> B;  a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)"
+     "\<lbrakk>A \<approx> B;  a \<notin> A;  b \<notin> B\<rbrakk> \<Longrightarrow> cons(a,A) \<approx> cons(b,B)"
 by (simp add: eqpoll_iff cons_lepoll_cong)
 
 lemma cons_lepoll_cons_iff:
-     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)  \<longleftrightarrow>  A \<lesssim> B"
+     "\<lbrakk>a \<notin> A;  b \<notin> B\<rbrakk> \<Longrightarrow> cons(a,A) \<lesssim> cons(b,B)  \<longleftrightarrow>  A \<lesssim> B"
 by (blast intro: cons_lepoll_cong cons_lepoll_consD)
 
 lemma cons_eqpoll_cons_iff:
-     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)  \<longleftrightarrow>  A \<approx> B"
+     "\<lbrakk>a \<notin> A;  b \<notin> B\<rbrakk> \<Longrightarrow> cons(a,A) \<approx> cons(b,B)  \<longleftrightarrow>  A \<approx> B"
 by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
 
 lemma singleton_eqpoll_1: "{a} \<approx> 1"
@@ -766,7 +766,7 @@
 apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
 done
 
-lemma not_0_is_lepoll_1: "A \<noteq> 0 ==> 1 \<lesssim> A"
+lemma not_0_is_lepoll_1: "A \<noteq> 0 \<Longrightarrow> 1 \<lesssim> A"
 apply (erule not_emptyE)
 apply (rule_tac a = "cons (x, A-{x}) " in subst)
 apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A-{x})" in subst)
@@ -774,26 +774,26 @@
 done
 
 (*Congruence law for  succ  under equipollence*)
-lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)"
+lemma succ_eqpoll_cong: "A \<approx> B \<Longrightarrow> succ(A) \<approx> succ(B)"
 apply (unfold succ_def)
 apply (simp add: cons_eqpoll_cong mem_not_refl)
 done
 
 (*Congruence law for + under equipollence*)
-lemma sum_eqpoll_cong: "[| A \<approx> C;  B \<approx> D |] ==> A+B \<approx> C+D"
+lemma sum_eqpoll_cong: "\<lbrakk>A \<approx> C;  B \<approx> D\<rbrakk> \<Longrightarrow> A+B \<approx> C+D"
 apply (unfold eqpoll_def)
 apply (blast intro!: sum_bij)
 done
 
 (*Congruence law for * under equipollence*)
 lemma prod_eqpoll_cong:
-    "[| A \<approx> C;  B \<approx> D |] ==> A*B \<approx> C*D"
+    "\<lbrakk>A \<approx> C;  B \<approx> D\<rbrakk> \<Longrightarrow> A*B \<approx> C*D"
 apply (unfold eqpoll_def)
 apply (blast intro!: prod_bij)
 done
 
 lemma inj_disjoint_eqpoll:
-    "[| f \<in> inj(A,B);  A \<inter> B = 0 |] ==> A \<union> (B - range(f)) \<approx> B"
+    "\<lbrakk>f \<in> inj(A,B);  A \<inter> B = 0\<rbrakk> \<Longrightarrow> A \<union> (B - range(f)) \<approx> B"
 apply (unfold eqpoll_def)
 apply (rule exI)
 apply (rule_tac c = "%x. if x \<in> A then f`x else x"
@@ -814,7 +814,7 @@
 text\<open>If \<^term>\<open>A\<close> has at most \<^term>\<open>n+1\<close> elements and \<^term>\<open>a \<in> A\<close>
       then \<^term>\<open>A-{a}\<close> has at most \<^term>\<open>n\<close>.\<close>
 lemma Diff_sing_lepoll:
-      "[| a \<in> A;  A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
+      "\<lbrakk>a \<in> A;  A \<lesssim> succ(n)\<rbrakk> \<Longrightarrow> A - {a} \<lesssim> n"
 apply (unfold succ_def)
 apply (rule cons_lepoll_consD)
 apply (rule_tac [3] mem_not_refl)
@@ -834,12 +834,12 @@
     by (blast intro: cons_lepoll_consD mem_irrefl)
 qed
 
-lemma Diff_sing_eqpoll: "[| a \<in> A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
+lemma Diff_sing_eqpoll: "\<lbrakk>a \<in> A; A \<approx> succ(n)\<rbrakk> \<Longrightarrow> A - {a} \<approx> n"
 by (blast intro!: eqpollI
           elim!: eqpollE
           intro: Diff_sing_lepoll lepoll_Diff_sing)
 
-lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a \<in> A |] ==> A = {a}"
+lemma lepoll_1_is_sing: "\<lbrakk>A \<lesssim> 1; a \<in> A\<rbrakk> \<Longrightarrow> A = {a}"
 apply (frule Diff_sing_lepoll, assumption)
 apply (drule lepoll_0_is_0)
 apply (blast elim: equalityE)
@@ -854,12 +854,12 @@
 done
 
 lemma well_ord_Un:
-     "[| well_ord(X,R); well_ord(Y,S) |] ==> \<exists>T. well_ord(X \<union> Y, T)"
+     "\<lbrakk>well_ord(X,R); well_ord(Y,S)\<rbrakk> \<Longrightarrow> \<exists>T. well_ord(X \<union> Y, T)"
 by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]],
     assumption)
 
 (*Krzysztof Grabczewski*)
-lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 ==> A \<union> B \<approx> A + B"
+lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 \<Longrightarrow> A \<union> B \<approx> A + B"
 apply (unfold eqpoll_def)
 apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI)
 apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective)
@@ -869,7 +869,7 @@
 
 subsection \<open>Finite and infinite sets\<close>
 
-lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
+lemma eqpoll_imp_Finite_iff: "A \<approx> B \<Longrightarrow> Finite(A) \<longleftrightarrow> Finite(B)"
 apply (unfold Finite_def)
 apply (blast intro: eqpoll_trans eqpoll_sym)
 done
@@ -879,7 +879,7 @@
 apply (blast intro!: eqpoll_refl nat_0I)
 done
 
-lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
+lemma Finite_cons: "Finite(x) \<Longrightarrow> Finite(cons(y,x))"
 apply (unfold Finite_def)
 apply (case_tac "y \<in> x")
 apply (simp add: cons_absorb)
@@ -889,7 +889,7 @@
 apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
 done
 
-lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
+lemma Finite_succ: "Finite(x) \<Longrightarrow> Finite(succ(x))"
 apply (unfold succ_def)
 apply (erule Finite_cons)
 done
@@ -911,7 +911,7 @@
 qed
 
 lemma lesspoll_nat_is_Finite:
-     "A \<prec> nat ==> Finite(A)"
+     "A \<prec> nat \<Longrightarrow> Finite(A)"
 apply (unfold Finite_def)
 apply (blast dest: ltD lesspoll_cardinal_lt
                    lesspoll_imp_eqpoll [THEN eqpoll_sym])
@@ -936,13 +936,13 @@
 lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)"
 by (simp add: succ_def)
 
-lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \<inter> B)"
+lemma Finite_Int: "Finite(A) | Finite(B) \<Longrightarrow> Finite(A \<inter> B)"
 by (blast intro: subset_Finite)
 
 lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
 
 lemma nat_le_infinite_Ord:
-      "[| Ord(i);  ~ Finite(i) |] ==> nat \<le> i"
+      "\<lbrakk>Ord(i);  \<not> Finite(i)\<rbrakk> \<Longrightarrow> nat \<le> i"
 apply (unfold Finite_def)
 apply (erule Ord_nat [THEN [2] Ord_linear2])
 prefer 2 apply assumption
@@ -950,19 +950,19 @@
 done
 
 lemma Finite_imp_well_ord:
-    "Finite(A) ==> \<exists>r. well_ord(A,r)"
+    "Finite(A) \<Longrightarrow> \<exists>r. well_ord(A,r)"
 apply (unfold Finite_def eqpoll_def)
 apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
 done
 
-lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
+lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y \<Longrightarrow> y \<noteq> 0"
 by (fast dest!: lepoll_0_is_0)
 
-lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
+lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) \<Longrightarrow> x \<noteq> 0"
 by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
 
 lemma Finite_Fin_lemma [rule_format]:
-     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) \<longrightarrow> A \<in> Fin(X)"
+     "n \<in> nat \<Longrightarrow> \<forall>A. (A\<approx>n & A \<subseteq> X) \<longrightarrow> A \<in> Fin(X)"
 apply (induct_tac n)
 apply (rule allI)
 apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
@@ -978,10 +978,10 @@
 apply (simp add: cons_Diff)
 done
 
-lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
+lemma Finite_Fin: "\<lbrakk>Finite(A); A \<subseteq> X\<rbrakk> \<Longrightarrow> A \<in> Fin(X)"
 by (unfold Finite_def, blast intro: Finite_Fin_lemma)
 
-lemma Fin_lemma [rule_format]: "n \<in> nat ==> \<forall>A. A \<approx> n \<longrightarrow> A \<in> Fin(A)"
+lemma Fin_lemma [rule_format]: "n \<in> nat \<Longrightarrow> \<forall>A. A \<approx> n \<longrightarrow> A \<in> Fin(A)"
 apply (induct_tac n)
 apply (simp add: eqpoll_0_iff, clarify)
 apply (subgoal_tac "\<exists>u. u \<in> A")
@@ -997,18 +997,18 @@
 apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
 done
 
-lemma Finite_into_Fin: "Finite(A) ==> A \<in> Fin(A)"
+lemma Finite_into_Fin: "Finite(A) \<Longrightarrow> A \<in> Fin(A)"
 apply (unfold Finite_def)
 apply (blast intro: Fin_lemma)
 done
 
-lemma Fin_into_Finite: "A \<in> Fin(U) ==> Finite(A)"
+lemma Fin_into_Finite: "A \<in> Fin(U) \<Longrightarrow> Finite(A)"
 by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
 
 lemma Finite_Fin_iff: "Finite(A) \<longleftrightarrow> A \<in> Fin(A)"
 by (blast intro: Finite_into_Fin Fin_into_Finite)
 
-lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A \<union> B)"
+lemma Finite_Un: "\<lbrakk>Finite(A); Finite(B)\<rbrakk> \<Longrightarrow> Finite(A \<union> B)"
 by (blast intro!: Fin_into_Finite Fin_UnI
           dest!: Finite_into_Fin
           intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
@@ -1018,7 +1018,7 @@
 by (blast intro: subset_Finite Finite_Un)
 
 text\<open>The converse must hold too.\<close>
-lemma Finite_Union: "[| \<forall>y\<in>X. Finite(y);  Finite(X) |] ==> Finite(\<Union>(X))"
+lemma Finite_Union: "\<lbrakk>\<forall>y\<in>X. Finite(y);  Finite(X)\<rbrakk> \<Longrightarrow> Finite(\<Union>(X))"
 apply (simp add: Finite_Fin_iff)
 apply (rule Fin_UnionI)
 apply (erule Fin_induct, simp)
@@ -1027,15 +1027,15 @@
 
 (* Induction principle for Finite(A), by Sidi Ehmety *)
 lemma Finite_induct [case_names 0 cons, induct set: Finite]:
-"[| Finite(A); P(0);
-    !! x B.   [| Finite(B); x \<notin> B; P(B) |] ==> P(cons(x, B)) |]
- ==> P(A)"
+"\<lbrakk>Finite(A); P(0);
+    \<And>x B.   \<lbrakk>Finite(B); x \<notin> B; P(B)\<rbrakk> \<Longrightarrow> P(cons(x, B))\<rbrakk>
+ \<Longrightarrow> P(A)"
 apply (erule Finite_into_Fin [THEN Fin_induct])
 apply (blast intro: Fin_into_Finite)+
 done
 
-(*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
-lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
+(*Sidi Ehmety.  The contrapositive says \<not>Finite(A) \<Longrightarrow> \<not>Finite(A-{a}) *)
+lemma Diff_sing_Finite: "Finite(A - {a}) \<Longrightarrow> Finite(A)"
 apply (unfold Finite_def)
 apply (case_tac "a \<in> A")
 apply (subgoal_tac [2] "A-{a}=A", auto)
@@ -1046,8 +1046,8 @@
 done
 
 (*Sidi Ehmety.  And the contrapositive of this says
-   [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
-lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) \<longrightarrow> Finite(A)"
+   \<lbrakk>\<not>Finite(A); Finite(B)\<rbrakk> \<Longrightarrow> \<not>Finite(A-B) *)
+lemma Diff_Finite [rule_format]: "Finite(B) \<Longrightarrow> Finite(A-B) \<longrightarrow> Finite(A)"
 apply (erule Finite_induct, auto)
 apply (case_tac "x \<in> A")
  apply (subgoal_tac [2] "A-cons (x, B) = A - B")
@@ -1055,12 +1055,12 @@
 apply (drule Diff_sing_Finite, auto)
 done
 
-lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
+lemma Finite_RepFun: "Finite(A) \<Longrightarrow> Finite(RepFun(A,f))"
 by (erule Finite_induct, simp_all)
 
 lemma Finite_RepFun_iff_lemma [rule_format]:
-     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|]
-      ==> \<forall>A. x = RepFun(A,f) \<longrightarrow> Finite(A)"
+     "\<lbrakk>Finite(x); \<And>x y. f(x)=f(y) \<Longrightarrow> x=y\<rbrakk>
+      \<Longrightarrow> \<forall>A. x = RepFun(A,f) \<longrightarrow> Finite(A)"
 apply (erule Finite_induct)
  apply clarify
  apply (case_tac "A=0", simp)
@@ -1078,15 +1078,15 @@
 text\<open>I don't know why, but if the premise is expressed using meta-connectives
 then  the simplifier cannot prove it automatically in conditional rewriting.\<close>
 lemma Finite_RepFun_iff:
-     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)"
+     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) \<Longrightarrow> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)"
 by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
 
-lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
+lemma Finite_Pow: "Finite(A) \<Longrightarrow> Finite(Pow(A))"
 apply (erule Finite_induct)
 apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
 done
 
-lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
+lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) \<Longrightarrow> Finite(A)"
 apply (subgoal_tac "Finite({{x} . x \<in> A})")
  apply (simp add: Finite_RepFun_iff )
 apply (blast intro: subset_Finite)
@@ -1103,7 +1103,7 @@
 (*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
   set is well-ordered.  Proofs simplified by lcp. *)
 
-lemma nat_wf_on_converse_Memrel: "n \<in> nat ==> wf[n](converse(Memrel(n)))"
+lemma nat_wf_on_converse_Memrel: "n \<in> nat \<Longrightarrow> wf[n](converse(Memrel(n)))"
 proof (induct n rule: nat_induct)
   case 0 thus ?case by (blast intro: wf_onI)
 next
@@ -1125,15 +1125,15 @@
     qed
 qed
 
-lemma nat_well_ord_converse_Memrel: "n \<in> nat ==> well_ord(n,converse(Memrel(n)))"
+lemma nat_well_ord_converse_Memrel: "n \<in> nat \<Longrightarrow> well_ord(n,converse(Memrel(n)))"
 apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
 apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) 
 done
 
 lemma well_ord_converse:
-     "[|well_ord(A,r);
-        well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |]
-      ==> well_ord(A,converse(r))"
+     "\<lbrakk>well_ord(A,r);
+        well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r))))\<rbrakk>
+      \<Longrightarrow> well_ord(A,converse(r))"
 apply (rule well_ord_Int_iff [THEN iffD1])
 apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
 apply (simp add: rvimage_converse converse_Int converse_prod
@@ -1153,16 +1153,16 @@
 qed
 
 lemma Finite_well_ord_converse:
-    "[| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))"
+    "\<lbrakk>Finite(A);  well_ord(A,r)\<rbrakk> \<Longrightarrow> well_ord(A,converse(r))"
 apply (unfold Finite_def)
 apply (rule well_ord_converse, assumption)
 apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
 done
 
-lemma nat_into_Finite: "n \<in> nat ==> Finite(n)"
+lemma nat_into_Finite: "n \<in> nat \<Longrightarrow> Finite(n)"
   by (auto simp add: Finite_def intro: eqpoll_refl) 
 
-lemma nat_not_Finite: "~ Finite(nat)"
+lemma nat_not_Finite: "\<not> Finite(nat)"
 proof -
   { fix n
     assume n: "n \<in> nat" "nat \<approx> n"