# HG changeset patch
# User huffman
# Date 1199394652 -3600
# Node ID c7b1e7b7087bc762ab1f97e9e8f4e897d49dd337
# Parent  eb181909e7a4aa7c9a57c12689f0f0be784106ff
instance unit :: finite_po

diff -r eb181909e7a4 -r c7b1e7b7087b src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Jan 03 22:09:44 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Jan 03 22:10:52 2008 +0100
@@ -27,8 +27,7 @@
 instance unit :: po
 by intro_classes simp_all
 
-instance unit :: dcpo
-by intro_classes (simp add: is_lub_def is_ub_def)
+instance unit :: finite_po ..
 
 instance unit :: pcpo
 by intro_classes simp