diff -r e44d86131648 -r 0c18df79b1c8 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/Order.thy	Tue Sep 27 17:03:23 2022 +0100
@@ -17,7 +17,7 @@
 
 definition
   part_ord :: "[i,i]=>o"                (*Strict partial ordering*)  where
-   "part_ord(A,r) \<equiv> irrefl(A,r) & trans[A](r)"
+   "part_ord(A,r) \<equiv> irrefl(A,r) \<and> trans[A](r)"
 
 definition
   linear   :: "[i,i]=>o"                (*Strict total ordering*)  where
@@ -25,7 +25,7 @@
 
 definition
   tot_ord  :: "[i,i]=>o"                (*Strict total ordering*)  where
-   "tot_ord(A,r) \<equiv> part_ord(A,r) & linear(A,r)"
+   "tot_ord(A,r) \<equiv> part_ord(A,r) \<and> linear(A,r)"
 
 definition
   "preorder_on(A, r) \<equiv> refl(A, r) \<and> trans[A](r)"
@@ -41,7 +41,7 @@
 
 definition
   well_ord :: "[i,i]=>o"                (*Well-ordering*)  where
-   "well_ord(A,r) \<equiv> tot_ord(A,r) & wf[A](r)"
+   "well_ord(A,r) \<equiv> tot_ord(A,r) \<and> wf[A](r)"
 
 definition
   mono_map :: "[i,i,i,i]=>i"            (*Order-preserving maps*)  where
@@ -64,7 +64,7 @@
 
 definition
   first :: "[i, i, i] => o"  where
-    "first(u, X, R) \<equiv> u \<in> X & (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)"
+    "first(u, X, R) \<equiv> u \<in> X \<and> (\<forall>v\<in>X. v\<noteq>u \<longrightarrow> <u,v> \<in> R)"
 
 subsection\<open>Immediate Consequences of the Definitions\<close>
 
@@ -102,7 +102,7 @@
 
 (** Derived rules for pred(A,x,r) **)
 
-lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r & y \<in> A"
+lemma pred_iff: "y \<in> pred(A,x,r) \<longleftrightarrow> <y,x>:r \<and> y \<in> A"
 by (unfold pred_def, blast)
 
 lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
@@ -474,7 +474,7 @@
          f \<in> ord_iso(A,r, B,s);  g \<in> ord_iso(A,r, B,s)\<rbrakk> \<Longrightarrow> f = g"
 apply (rule fun_extension)
 apply (erule ord_iso_is_bij [THEN bij_is_fun])+
-apply (subgoal_tac "f`x \<in> B & g`x \<in> B & linear(B,s)")
+apply (subgoal_tac "f`x \<in> B \<and> g`x \<in> B \<and> linear(B,s)")
  apply (simp add: linear_def)
  apply (blast dest: well_ord_iso_unique_lemma)
 apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype
@@ -517,7 +517,7 @@
 apply (unfold mono_map_def)
 apply (simp (no_asm_simp) add: ord_iso_map_fun)
 apply safe
-apply (subgoal_tac "x \<in> A & ya:A & y \<in> B & yb:B")
+apply (subgoal_tac "x \<in> A \<and> ya:A \<and> y \<in> B \<and> yb:B")
  apply (simp add: apply_equality [OF _  ord_iso_map_fun])
  apply (unfold ord_iso_map_def)
  apply (blast intro: well_ord_iso_preserving, blast)