src/HOLCF/Lift1.thy
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 *)