Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOLCF/Lift1.thy: now imports Sum
authorlcp
Mon, 22 Aug 1994 11:03:52 +0200
changeset 569 4dc184a3d09b
parent 568 756b0e2a6cac
child 570 6333c181a3f7
HOLCF/Lift1.thy: now imports Sum
src/HOLCF/Lift1.thy file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle