--- 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)"