# HG changeset patch
# User huffman
# Date 1214874759 -7200
# Node ID be852e06d546d4321640e93d6ac202edd481534c
# Parent  95ec4bda5bb9850b89451a7ab2b30f2d181e59e4
remove redundant instance proof finite_po < cpo

diff -r 95ec4bda5bb9 -r be852e06d546 src/HOLCF/Pcpo.thy
--- 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 *}