--- a/src/HOL/Library/Primes.thy Sun Jan 13 21:13:59 2002 +0100
+++ b/src/HOL/Library/Primes.thy Sun Jan 13 21:14:14 2002 +0100
@@ -188,12 +188,13 @@
*}
lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
- apply (blast intro: relprime_dvd_mult prime_imp_relprime)
- done
+ by (blast intro: relprime_dvd_mult prime_imp_relprime)
lemma prime_dvd_square: "p \<in> prime ==> p dvd m^Suc (Suc 0) ==> p dvd m"
- apply (auto dest: prime_dvd_mult)
- done
+ by (auto dest: prime_dvd_mult)
+
+lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
+ by (rule prime_dvd_square) (simp_all add: power_two)
text {* \medskip Addition laws *}