src/HOL/Int.thy

--- a/src/HOL/Int.thy	Wed Oct 22 14:15:42 2008 +0200
+++ b/src/HOL/Int.thy	Wed Oct 22 14:15:43 2008 +0200
@@ -21,9 +21,7 @@
 
 subsection {* The equivalence relation underlying the integers *}
 
-definition
-  intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
-where
+definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
   [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
 
 typedef (Integ)