Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
instance unit :: finite_po
authorhuffman
Thu, 03 Jan 2008 22:10:52 +0100
changeset 25815 c7b1e7b7087b
parent 25814 eb181909e7a4
child 25816 d2a94e6a7d1e
instance unit :: finite_po
src/HOLCF/Cprod.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle