diff -r f2094906e491 -r e44d86131648 src/ZF/Induct/Rmap.thy
--- a/src/ZF/Induct/Rmap.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Induct/Rmap.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -15,12 +15,12 @@
   intros
     NilI:  "<Nil,Nil> \<in> rmap(r)"
 
-    ConsI: "[| <x,y>: r;  <xs,ys> \<in> rmap(r) |]
-            ==> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
+    ConsI: "\<lbrakk><x,y>: r;  <xs,ys> \<in> rmap(r)\<rbrakk>
+            \<Longrightarrow> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
 
   type_intros domainI rangeI list.intros
 
-lemma rmap_mono: "r \<subseteq> s ==> rmap(r) \<subseteq> rmap(s)"
+lemma rmap_mono: "r \<subseteq> s \<Longrightarrow> rmap(r) \<subseteq> rmap(s)"
   apply (unfold rmap.defs)
   apply (rule lfp_mono)
     apply (rule rmap.bnd_mono)+
@@ -33,19 +33,19 @@
 
 declare rmap.intros [intro]
 
-lemma rmap_rel_type: "r \<subseteq> A \<times> B ==> rmap(r) \<subseteq> list(A) \<times> list(B)"
+lemma rmap_rel_type: "r \<subseteq> A \<times> B \<Longrightarrow> rmap(r) \<subseteq> list(A) \<times> list(B)"
   apply (rule rmap.dom_subset [THEN subset_trans])
   apply (assumption |
     rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
   done
 
-lemma rmap_total: "A \<subseteq> domain(r) ==> list(A) \<subseteq> domain(rmap(r))"
+lemma rmap_total: "A \<subseteq> domain(r) \<Longrightarrow> list(A) \<subseteq> domain(rmap(r))"
   apply (rule subsetI)
   apply (erule list.induct)
    apply blast+
   done
 
-lemma rmap_functional: "function(r) ==> function(rmap(r))"
+lemma rmap_functional: "function(r) \<Longrightarrow> function(rmap(r))"
   apply (unfold function_def)
   apply (rule impI [THEN allI, THEN allI])
   apply (erule rmap.induct)
@@ -57,14 +57,14 @@
   as expected.
 \<close>
 
-lemma rmap_fun_type: "f \<in> A->B ==> rmap(f): list(A)->list(B)"
+lemma rmap_fun_type: "f \<in> A->B \<Longrightarrow> rmap(f): list(A)->list(B)"
   by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
 
 lemma rmap_Nil: "rmap(f)`Nil = Nil"
   by (unfold apply_def) blast
 
-lemma rmap_Cons: "[| f \<in> A->B;  x \<in> A;  xs: list(A) |]
-      ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
+lemma rmap_Cons: "\<lbrakk>f \<in> A->B;  x \<in> A;  xs: list(A)\<rbrakk>
+      \<Longrightarrow> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
   by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
 
 end