| changeset 1824 | 44254696843a |
| parent 1496 | c443b2adaf52 |
| child 2740 | 2c549ae2563b |
| 1823:e1458e1a9f80 | 1824:44254696843a |
|---|---|
9 RelPow = Nat + |
9 RelPow = Nat + |
10 |
10 |
11 consts |
11 consts |
12 "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100) |
12 "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100) |
13 defs |
13 defs |
14 rel_pow_def "R^n == nat_rec n id (%m S. R O S)" |
14 rel_pow_def "R^n == nat_rec id (%m S. R O S) n" |
15 end |
15 end |