# HG changeset patch
# User nipkow
# Date 1327956581 -3600
# Node ID 6fa9cdb8b850167a5e5e84518deaaa67c3672306
# Parent  b3e53dd6f10a301b0bbf07ede2bfbf547e6ac33f
added "'a rel"

diff -r b3e53dd6f10a -r 6fa9cdb8b850 src/HOL/Relation.thy
--- 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