| changeset 1401 | 0c439768f45c |
| parent 1155 | 928a16e02f9f |
| child 1478 | 2b8c2a7547ab |
| 1400:5d909faf0e04 | 1401:0c439768f45c |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 Rmap = List + |
9 Rmap = List + |
10 |
10 |
11 consts |
11 consts |
12 rmap :: "i=>i" |
12 rmap :: i=>i |
13 |
13 |
14 inductive |
14 inductive |
15 domains "rmap(r)" <= "list(domain(r))*list(range(r))" |
15 domains "rmap(r)" <= "list(domain(r))*list(range(r))" |
16 intrs |
16 intrs |
17 NilI "<Nil,Nil> : rmap(r)" |
17 NilI "<Nil,Nil> : rmap(r)" |