| changeset 65449 | c82e63b11b8b |
| parent 61798 | 27f3c10b0b50 |
| child 76213 | e44d86131648 |
| 65448:9bc3b57c1fa7 | 65449:c82e63b11b8b |
|---|---|
3 Copyright 1994 University of Cambridge |
3 Copyright 1994 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section \<open>An operator to ``map'' a relation over a list\<close> |
6 section \<open>An operator to ``map'' a relation over a list\<close> |
7 |
7 |
8 theory Rmap imports Main begin |
8 theory Rmap imports ZF begin |
9 |
9 |
10 consts |
10 consts |
11 rmap :: "i=>i" |
11 rmap :: "i=>i" |
12 |
12 |
13 inductive |
13 inductive |