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