diff -r 33b9b5da3e6f -r 119391dd1d59 src/HOLCF/One.thy
--- a/src/HOLCF/One.thy	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/One.thy	Thu Oct 06 18:40:18 1994 +0100
@@ -3,27 +3,17 @@
     Author: 	Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Introduve atomic type one = (void)u
+Introduce atomic type one = (void)u
 
-This is the first type that is introduced using a domain isomorphism.
-The type axiom 
-
-	arities one :: pcpo
+The type is axiomatized as the least solution of a domain equation.
+The functor term that specifies the domain equation is: 
 
-and the continuity of the Isomorphisms are taken for granted. Since the
-type is not recursive, it could be easily introduced in a purely conservative
-style as it was used for the types sprod, ssum, lift. The definition of the 
-ordering is canonical using abstraction and representation, but this would take
-again a lot of internal constants. It can easily be seen that the axioms below
-are consistent.
+  FT = <U,K_{void}>
 
-The partial ordering on type one is implicitly defined via the
-isomorphism axioms and the continuity of abs_one and rep_one.
+For details see chapter 5 of:
 
-We could also introduce the function less_one with definition
-
-less_one(x,y) = rep_one[x] << rep_one[y]
-
+[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
+                     Dissertation, Technische Universit"at M"unchen, 1994
 
 *)