# HG changeset patch # User lcp # Date 777546232 -7200 # Node ID 4dc184a3d09b427f138dd577dd81a604ec450926 # Parent 756b0e2a6cac6ffc92752591cd73b37695fc3912 HOLCF/Lift1.thy: now imports Sum diff -r 756b0e2a6cac -r 4dc184a3d09b src/HOLCF/Lift1.thy --- 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 *)