equal
deleted
inserted
replaced
11 This means that it may be necessary to attach explicit type constraints. |
11 This means that it may be necessary to attach explicit type constraints. |
12 Examples: range(f^n) = A and Range(R^n) = B need constraints. |
12 Examples: range(f^n) = A and Range(R^n) = B need constraints. |
13 *) |
13 *) |
14 |
14 |
15 theory Relation_Power |
15 theory Relation_Power |
16 import Nat |
16 imports Nat |
17 begin |
17 begin |
18 |
18 |
19 instance |
19 instance |
20 set :: (type) power .. (* only ('a * 'a) set should be in power! *) |
20 set :: (type) power .. (* only ('a * 'a) set should be in power! *) |
21 |
21 |