--- a/src/HOL/Old_Number_Theory/Primes.thy Tue Oct 21 17:23:16 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Primes.thy Tue Oct 21 21:10:44 2014 +0200
@@ -68,7 +68,7 @@
proof-
from e have np: "n > 0" by presburger
from e have "2 dvd (n - 1)" by presburger
- then obtain k where "n - 1 = 2*k" using dvd_def by auto
+ then obtain k where "n - 1 = 2 * k" ..
hence k: "n = 2*k + 1" using e by presburger
hence "n\<^sup>2 = 4* (k\<^sup>2 + k) + 1" by algebra
thus ?thesis by blast
@@ -588,7 +588,6 @@
thus ?thesis by blast
qed
-lemma even_dvd[simp]: "even (n::nat) \<longleftrightarrow> 2 dvd n" by presburger
lemma prime_odd: "prime p \<Longrightarrow> p = 2 \<or> odd p" unfolding prime_def by auto
@@ -828,6 +827,5 @@
done
declare power_Suc0[simp del]
-declare even_dvd[simp del]
end