# 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 *)