src/HOL/Number_Theory/Residues.thy
changeset 63633 2accfb71e33b
parent 63537 831816778409
child 64272 f76b6dda2e56
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Aug 08 14:13:14 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Aug 08 17:47:51 2016 +0200
     1.3 @@ -280,7 +280,7 @@
     1.4    qed
     1.5    then show ?thesis
     1.6      using \<open>2 \<le> p\<close>
     1.7 -    by (simp add: is_prime_nat_iff)
     1.8 +    by (simp add: prime_nat_iff)
     1.9         (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
    1.10                not_numeral_le_zero one_dvd)
    1.11  qed