src/HOL/Library/Primes.thy
changeset 14353 79f9fbef9106
parent 13187 e5434b822a96
child 14706 71590b7733b7
     1.1 --- a/src/HOL/Library/Primes.thy	Mon Jan 12 16:45:35 2004 +0100
     1.2 +++ b/src/HOL/Library/Primes.thy	Mon Jan 12 16:51:45 2004 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4    by (auto dest: prime_dvd_mult)
     1.5  
     1.6  lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
     1.7 -  by (rule prime_dvd_square) (simp_all add: power_two)
     1.8 +  by (rule prime_dvd_square) (simp_all add: power2_eq_square)
     1.9  
    1.10  
    1.11  text {* \medskip Addition laws *}