changeset 19086 | 1b3780be6cc2 |
parent 16762 | aafd23b47a5d |
child 21256 | 47195501ecf7 |
--- a/src/HOL/Library/Primes.thy Thu Feb 16 21:11:58 2006 +0100 +++ b/src/HOL/Library/Primes.thy Thu Feb 16 21:12:00 2006 +0100 @@ -10,12 +10,12 @@ imports Main begin -constdefs +definition coprime :: "nat => nat => bool" - "coprime m n == gcd (m, n) = 1" + "coprime m n = (gcd (m, n) = 1)" prime :: "nat \<Rightarrow> bool" - "prime p == 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)" + "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))" lemma two_is_prime: "prime 2"