| changeset 569 | 4dc184a3d09b |
| parent 542 | 164be35c8a16 |
| child 1150 | 66512c9e6bd6 |
--- a/src/HOLCF/Lift1.thy Fri Aug 19 16:13:53 1994 +0200 +++ b/src/HOLCF/Lift1.thy Mon Aug 22 11:03:52 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: HOLCF/lift1.thy +(* Title: HOLCF/Lift1.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen @@ -8,7 +8,7 @@ *) -Lift1 = Cfun3 + +Lift1 = Cfun3 + Sum + (* new type for lifting *)