# HG changeset patch
# User huffman
# Date 1199401107 -3600
# Node ID 94c075b912ffbff2cb30397406a55c33dbb4fc05
# Parent  f56dd9745d1b542cf7af991c7b55efa50fba2a91
generalized chfindom_monofun2cont

diff -r f56dd9745d1b -r 94c075b912ff src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Thu Jan 03 23:19:30 2008 +0100
+++ b/src/HOLCF/Cont.thy	Thu Jan 03 23:58:27 2008 +0100
@@ -189,7 +189,7 @@
   "\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
 by (rule cont2mono [THEN monofun_finch2finch])
 
-lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::pcpo)"
+lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
 apply (rule monocontlub2cont)
 apply assumption
 apply (rule contlubI)