# HG changeset patch
# User wenzelm
# Date 1010952854 -3600
# Node ID 1fce8f51034dbcc2c47ccef40c44f39701d6eeb5
# Parent  9d80e3746eb0d1e6b8e6664098cf1bd6f70eca0d
prime_dvd_power_two;

diff -r 9d80e3746eb0 -r 1fce8f51034d src/HOL/Library/Primes.thy
--- 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 *}