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