| changeset 8122 | b43ad07660b9 |
| parent 8041 | e3237d8c18d6 |
| child 8251 | 9be357df93d4 |
| 8121:4a53041acb28 | 8122:b43ad07660b9 |
|---|---|
4 Copyright 1999 University of Cambridge |
4 Copyright 1999 University of Cambridge |
5 |
5 |
6 lift_prog, etc: replication of components |
6 lift_prog, etc: replication of components |
7 *) |
7 *) |
8 |
8 |
9 Lift_prog = ELT + |
9 Lift_prog = Project + |
10 |
10 |
11 constdefs |
11 constdefs |
12 |
12 |
13 lift_map :: "['a, 'b * ('a => 'b)] => ('a => 'b)" |
13 lift_map :: "['a, 'b * ('a => 'b)] => ('a => 'b)" |
14 "lift_map i == %(s,f). f(i := s)" |
14 "lift_map i == %(s,f). f(i := s)" |