| changeset 14353 | 79f9fbef9106 |
| parent 13187 | e5434b822a96 |
| child 14706 | 71590b7733b7 |
--- a/src/HOL/Library/Primes.thy Mon Jan 12 16:45:35 2004 +0100 +++ b/src/HOL/Library/Primes.thy Mon Jan 12 16:51:45 2004 +0100 @@ -200,7 +200,7 @@ 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) + by (rule prime_dvd_square) (simp_all add: power2_eq_square) text {* \medskip Addition laws *}