changeset 61762 | d50b993b4fb9 |
parent 61076 | bdc1e2f0a86a |
child 61954 | 1d43f86f48be |
--- a/src/HOL/Proofs/Extraction/Euclid.thy Mon Nov 30 14:24:51 2015 +0100 +++ b/src/HOL/Proofs/Extraction/Euclid.thy Tue Dec 01 14:09:10 2015 +0000 @@ -29,7 +29,7 @@ by (induct m) auto lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))" - apply (simp add: prime_nat_def) + apply (simp add: prime_def) apply (rule iffI) apply blast apply (erule conjE)