--- a/src/HOLCF/One.thy Wed May 25 09:04:24 2005 +0200
+++ b/src/HOLCF/One.thy Wed May 25 09:44:34 2005 +0200
@@ -1,7 +1,8 @@
(* Title: HOLCF/One.thy
ID: $Id$
Author: Oscar Slotosch
- License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+The unit domain.
*)
header {* The unit domain *}
@@ -19,14 +20,6 @@
translations
"one" <= (type) "unit lift"
-(* Title: HOLCF/One.ML
- ID: $Id$
- Author: Oscar Slotosch
- License: GPL (GNU GENERAL PUBLIC LICENSE)
-
-The unit domain.
-*)
-
(* ------------------------------------------------------------------------ *)
(* Exhaustion and Elimination for type one *)
(* ------------------------------------------------------------------------ *)