| changeset 25815 | c7b1e7b7087b |
| parent 25784 | 71157f7e671e |
| child 25827 | c2adeb1bae5c |
--- 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