src/HOL/Library/Primes.thy

--- a/src/HOL/Library/Primes.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/Primes.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -11,10 +11,11 @@
 begin
 
 definition
-  coprime :: "nat => nat => bool"
+  coprime :: "nat => nat => bool" where
   "coprime m n = (gcd (m, n) = 1)"
 
-  prime :: "nat \<Rightarrow> bool"
+definition
+  prime :: "nat \<Rightarrow> bool" where
   "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"