--- a/src/HOL/Divides.thy Sun May 06 18:20:25 2018 +0000
+++ b/src/HOL/Divides.thy Sun May 06 18:20:25 2018 +0000
@@ -1295,10 +1295,6 @@
subsubsection \<open>Lemmas of doubtful value\<close>
-lemma mod_mult_self3':
- "Suc (k * n + m) mod n = Suc m mod n"
- by (fact Suc_mod_mult_self3)
-
lemma mod_Suc_eq_Suc_mod:
"Suc m mod n = Suc (m mod n) mod n"
by (simp add: mod_simps)
@@ -1327,16 +1323,6 @@
then show ?thesis ..
qed
-lemmas even_times_iff = even_mult_iff \<comment> \<open>FIXME duplicate\<close>
-
-lemma mod_2_not_eq_zero_eq_one_nat:
- fixes n :: nat
- shows "n mod 2 \<noteq> 0 \<longleftrightarrow> n mod 2 = 1"
- by (fact not_mod_2_eq_0_eq_1)
-
-lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
- by (fact even_of_nat)
-
lemma is_unit_int:
"is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
by auto