src/HOLCF/Cprod.thy
changeset 25815 c7b1e7b7087b
parent 25784 71157f7e671e
child 25827 c2adeb1bae5c
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Jan 03 22:09:44 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Jan 03 22:10:52 2008 +0100
     1.3 @@ -27,8 +27,7 @@
     1.4  instance unit :: po
     1.5  by intro_classes simp_all
     1.6  
     1.7 -instance unit :: dcpo
     1.8 -by intro_classes (simp add: is_lub_def is_ub_def)
     1.9 +instance unit :: finite_po ..
    1.10  
    1.11  instance unit :: pcpo
    1.12  by intro_classes simp