changeset 67226 | ec32cdaab97b |
parent 67118 | ccab07d1196c |
child 67816 | 2249b27ab1dd |
--- a/src/HOL/Divides.thy Tue Dec 19 14:51:27 2017 +0100 +++ b/src/HOL/Divides.thy Tue Dec 19 13:58:12 2017 +0100 @@ -1327,7 +1327,7 @@ then show ?thesis .. qed -lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close> +lemmas even_times_iff = even_mult_iff \<comment> \<open>FIXME duplicate\<close> lemma mod_2_not_eq_zero_eq_one_nat: fixes n :: nat