src/HOL/Relation.thy
changeset 46372 6fa9cdb8b850
parent 46127 af3b95160b59
child 46635 cde737f9c911
     1.1 --- a/src/HOL/Relation.thy	Mon Jan 30 17:18:58 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Jan 30 21:49:41 2012 +0100
     1.3 @@ -11,6 +11,8 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 +type_synonym 'a rel = "('a * 'a) set"
     1.8 +
     1.9  definition
    1.10    converse :: "('a * 'b) set => ('b * 'a) set"
    1.11      ("(_^-1)" [1000] 999) where