--- 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