| changeset 24915 | fc90277c0dd7 |
| parent 24286 | 7619080e49f0 |
| child 26271 | e324f8918c98 |
| 24914:95cda5dd58d5 | 24915:fc90277c0dd7 |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Relations *} |
7 header {* Relations *} |
8 |
8 |
9 theory Relation |
9 theory Relation |
10 imports Product_Type FixedPoint |
10 imports Product_Type |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definitions *} |
13 subsection {* Definitions *} |
14 |
14 |
15 definition |
15 definition |