# HG changeset patch
# User nipkow
# Date 1327990280 -3600
# Node ID 10c5f39ec7764b78e1c7466c745383f20ee1785e
# Parent  e2b1a86d59fc98a1b135c235b3c1d72e67edbe0f# Parent  d4afc422668868e7a2fe384714709237041e6436
merged

diff -r e2b1a86d59fc -r 10c5f39ec776 NEWS
--- a/NEWS	Mon Jan 30 22:56:09 2012 +0100
+++ b/NEWS	Tue Jan 31 07:11:20 2012 +0100
@@ -73,6 +73,8 @@
 predicate and what a set.  It can be helpful to carry out that step in
 Isabelle2011-1 before jumping right into the current release.
 
+* New type synonym 'a rel = ('a * 'a) set
+
 * Consolidated various theorem names relating to Finite_Set.fold
 combinator:
 
diff -r e2b1a86d59fc -r 10c5f39ec776 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Jan 30 22:56:09 2012 +0100
+++ b/src/HOL/Relation.thy	Tue Jan 31 07:11:20 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