| changeset 8844 | db71c334e854 |
| parent 5780 | 0187f936685a |
| 8843:5370a030dd47 | 8844:db71c334e854 |
|---|---|
9 RelPow = Nat + |
9 RelPow = Nat + |
10 |
10 |
11 instance |
11 instance |
12 set :: (term) {power} (* only ('a * 'a) set should be in power! *) |
12 set :: (term) {power} (* only ('a * 'a) set should be in power! *) |
13 |
13 |
14 primrec |
14 primrec (relpow) |
15 "R^0 = Id" |
15 "R^0 = Id" |
16 "R^(Suc n) = R O (R^n)" |
16 "R^(Suc n) = R O (R^n)" |
17 |
17 |
18 end |
18 end |