| changeset 53015 | a1119cf551e8 |
| parent 50037 | f2a32197a33a |
| child 53077 | a1b3784f8129 |
--- a/src/HOL/Old_Number_Theory/Primes.thy Tue Aug 13 14:20:22 2013 +0200 +++ b/src/HOL/Old_Number_Theory/Primes.thy Tue Aug 13 16:25:47 2013 +0200 @@ -39,7 +39,7 @@ lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m" by (auto dest: prime_dvd_mult) -lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m" +lemma prime_dvd_power_two: "prime p ==> p dvd m\<^sup>2 ==> p dvd m" by (rule prime_dvd_square) (simp_all add: power2_eq_square)