| changeset 569 | 4dc184a3d09b |
| parent 542 | 164be35c8a16 |
| child 1150 | 66512c9e6bd6 |
| 568:756b0e2a6cac | 569:4dc184a3d09b |
|---|---|
1 (* Title: HOLCF/lift1.thy |
1 (* Title: HOLCF/Lift1.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 |
6 |
7 Lifting |
7 Lifting |
8 |
8 |
9 *) |
9 *) |
10 |
10 |
11 Lift1 = Cfun3 + |
11 Lift1 = Cfun3 + Sum + |
12 |
12 |
13 (* new type for lifting *) |
13 (* new type for lifting *) |
14 |
14 |
15 types "u" 1 |
15 types "u" 1 |
16 |
16 |