src/HOL/ex/Sqrt.thy

 
 theorem sqrt_prime_irrational:
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
     and "coprime m n" by (rule Rats_abs_nat_div_natE)
   have eq: "m\<^sup>2 = p * n\<^sup>2"

 
 theorem
   assumes "prime (p::nat)"
   shows "sqrt p \<notin> \<rat>"
 proof
-  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
+  from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
     and "coprime m n" by (rule Rats_abs_nat_div_natE)
   from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp