diff -r 4dcccaa11a13 -r 861a255cf1e7 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu May 19 01:22:53 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Thu May 19 02:33:40 2005 +0200
@@ -14,6 +14,23 @@
 
 defaultsort cpo
 
+subsection {* Type @{typ unit} is a pcpo *}
+
+instance unit :: sq_ord ..
+
+defs (overloaded)
+  less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
+
+instance unit :: po
+by intro_classes simp_all
+
+instance unit :: cpo
+by intro_classes (simp add: is_lub_def is_ub_def)
+
+instance unit :: pcpo
+by intro_classes simp
+
+
 subsection {* Ordering on @{typ "'a * 'b"} *}
 
 instance "*" :: (sq_ord, sq_ord) sq_ord ..