diff -r e44d86131648 -r 0c18df79b1c8 src/ZF/Induct/Mutil.thy
--- a/src/ZF/Induct/Mutil.thy	Tue Sep 27 16:51:35 2022 +0100
+++ b/src/ZF/Induct/Mutil.thy	Tue Sep 27 17:03:23 2022 +0100
@@ -38,7 +38,7 @@
 
 subsection \<open>Basic properties of evnodd\<close>
 
-lemma evnodd_iff: "<i,j>: evnodd(A,b) \<longleftrightarrow> <i,j>: A & (i#+j) mod 2 = b"
+lemma evnodd_iff: "<i,j>: evnodd(A,b) \<longleftrightarrow> <i,j>: A \<and> (i#+j) mod 2 = b"
   by (unfold evnodd_def) blast
 
 lemma evnodd_subset: "evnodd(A, b) \<subseteq> A"