| changeset 8041 | e3237d8c18d6 |
| parent 7947 | b999c1ab9327 |
| child 8122 | b43ad07660b9 |
| 8040:23e2a2457c77 | 8041:e3237d8c18d6 |
|---|---|
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 = Project + |
9 Lift_prog = ELT + |
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)" |