changeset 16417 | 9bc16273c2d4 |
parent 12610 | 8b9845807f77 |
child 35762 | af3ff2ba4c54 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 header {* An operator to ``map'' a relation over a list *} |
7 header {* An operator to ``map'' a relation over a list *} |
8 |
8 |
9 theory Rmap = Main: |
9 theory Rmap imports Main begin |
10 |
10 |
11 consts |
11 consts |
12 rmap :: "i=>i" |
12 rmap :: "i=>i" |
13 |
13 |
14 inductive |
14 inductive |