equal
deleted
inserted
replaced
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* Relations *} |
7 header {* Relations *} |
8 |
8 |
9 theory Relation = Product_Type: |
9 theory Relation |
|
10 import Product_Type |
|
11 begin |
10 |
12 |
11 subsection {* Definitions *} |
13 subsection {* Definitions *} |
12 |
14 |
13 constdefs |
15 constdefs |
14 converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999) |
16 converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999) |