--- a/src/HOLCF/One.thy Fri Mar 04 23:12:36 2005 +0100
+++ b/src/HOLCF/One.thy Fri Mar 04 23:23:47 2005 +0100
@@ -4,7 +4,11 @@
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
-theory One = Lift:
+header {* The unit domain *}
+
+theory One
+imports Lift
+begin
types one = "unit lift"