changeset 63633 | 2accfb71e33b |
parent 63537 | 831816778409 |
child 63830 | 2ea3725a34bd |
--- a/src/HOL/Proofs/Extraction/Euclid.thy Mon Aug 08 14:13:14 2016 +0200 +++ b/src/HOL/Proofs/Extraction/Euclid.thy Mon Aug 08 17:47:51 2016 +0200 @@ -28,7 +28,7 @@ by (induct m) auto lemma prime_eq: "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)" - apply (simp add: is_prime_nat_iff) + apply (simp add: prime_nat_iff) apply (rule iffI) apply blast apply (erule conjE)