added "'a rel"

--- a/src/HOL/Relation.thy	Mon Jan 30 17:18:58 2012 +0100
+++ b/src/HOL/Relation.thy	Mon Jan 30 21:49:41 2012 +0100
@@ -11,6 +11,8 @@
 
 subsection {* Definitions *}
 
+type_synonym 'a rel = "('a * 'a) set"
+
 definition
   converse :: "('a * 'b) set => ('b * 'a) set"
     ("(_^-1)" [1000] 999) where