--- a/src/HOLCF/Pcpo.thy Tue Jul 01 02:50:29 2008 +0200
+++ b/src/HOLCF/Pcpo.thy Tue Jul 01 03:12:39 2008 +0200
@@ -263,7 +263,7 @@
axclass flat < pcpo
ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
-text {* finite partial orders are chain-finite and directed-complete *}
+text {* finite partial orders are chain-finite *}
instance finite_po < chfin
apply intro_classes
@@ -272,14 +272,6 @@
apply (simp add: finite_chain_def)
done
-instance finite_po < cpo
-apply intro_classes
-apply (drule directed_chain)
-apply (drule directed_finiteD [OF _ finite subset_refl])
-apply (erule bexE, rule exI)
-apply (erule (1) is_lub_maximal)
-done
-
text {* some properties for chfin and flat *}
text {* chfin types are cpo *}