| changeset 76214 | 0c18df79b1c8 |
| parent 76213 | e44d86131648 |
| child 76215 | a642599ffdea |
--- 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"