src/HOL/Library/GCD.thy

--- a/src/HOL/Library/GCD.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/GCD.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -22,7 +22,7 @@
   "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
 
 definition
-  is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
+  is_gcd :: "nat => nat => nat => bool" where -- {* @{term gcd} as a relation *}
   "is_gcd p m n = (p dvd m \<and> p dvd n \<and>
     (\<forall>d. d dvd m \<and> d dvd n --> d dvd p))"