| changeset 60804 | 080a979a985b |
| parent 60688 | 01488b559910 |
| child 61762 | d50b993b4fb9 |
--- a/src/HOL/Number_Theory/Primes.thy Mon Jul 27 22:08:46 2015 +0200 +++ b/src/HOL/Number_Theory/Primes.thy Mon Jul 27 22:44:02 2015 +0200 @@ -35,7 +35,7 @@ declare [[coercion_enabled]] definition prime :: "nat \<Rightarrow> bool" - where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" + where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))" lemmas prime_nat_def = prime_def