| changeset 26072 | f65a7fa2da6c |
| parent 25861 | 494d9301cc75 |
| child 26799 | 5bd38256ce5b |
| 26071:046fe7ddfc4b | 26072:f65a7fa2da6c |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header{*Powers of Relations and Functions*} |
7 header{*Powers of Relations and Functions*} |
8 |
8 |
9 theory Relation_Power |
9 theory Relation_Power |
10 imports Power |
10 imports Power Transitive_Closure |
11 begin |
11 begin |
12 |
12 |
13 instance |
13 instance |
14 set :: (type) power .. |
14 set :: (type) power .. |
15 --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*} |
15 --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*} |