equal
deleted
inserted
replaced
13 *) |
13 *) |
14 |
14 |
15 Relation_Power = Nat + |
15 Relation_Power = Nat + |
16 |
16 |
17 instance |
17 instance |
18 set :: (term) {power} (* only ('a * 'a) set should be in power! *) |
18 set :: (type) power (* only ('a * 'a) set should be in power! *) |
19 |
19 |
20 primrec (relpow) |
20 primrec (relpow) |
21 "R^0 = Id" |
21 "R^0 = Id" |
22 "R^(Suc n) = R O (R^n)" |
22 "R^(Suc n) = R O (R^n)" |
23 |
23 |
24 |
24 |
25 instance |
25 instance |
26 fun :: (term,term)power (* only 'a => 'a should be in power! *) |
26 fun :: (type, type) power (* only 'a => 'a should be in power! *) |
27 |
27 |
28 primrec (funpow) |
28 primrec (funpow) |
29 "f^0 = id" |
29 "f^0 = id" |
30 "f^(Suc n) = f o (f^n)" |
30 "f^(Suc n) = f o (f^n)" |
31 |
31 |