src/HOL/ex/Sqrt_Script.thy
changeset 63534 523b488b15c9
parent 61933 cf58b5b794b2
child 63635 858a225ebb62
--- a/src/HOL/ex/Sqrt_Script.thy	Wed Jul 20 14:52:09 2016 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy	Thu Jul 21 10:06:04 2016 +0200
@@ -17,7 +17,7 @@
 subsection \<open>Preliminaries\<close>
 
 lemma prime_nonzero:  "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
-  by (force simp add: prime_def)
+  by (force simp add: is_prime_nat_iff)
 
 lemma prime_dvd_other_side:
     "(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
@@ -32,7 +32,7 @@
   apply (erule disjE)
    apply (frule mult_le_mono, assumption)
    apply auto
-  apply (force simp add: prime_def)
+  apply (force simp add: is_prime_nat_iff)
   done
 
 lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"