src/HOLCF/Cont.ML

         (etac (is_chainE RS spec) 1)
         ]);
 
 
 qed_goal "ch2ch_lubMF2R" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F);is_chain(Y)|] ==> \
 \       is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),

         (atac 1)
         ]);
 
 
 qed_goal "ch2ch_lubMF2L" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F);is_chain(Y)|] ==> \
 \       is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),

         (atac 1)
         ]);
 
 
 qed_goal "lub_MF2_mono" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F)|] ==> \
 \       monofun(% x.lub(range(% j.MF2 (F j) (x))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),

         ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)),
         (atac 1)
         ]);
 
 qed_goal "ex_lubMF2" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F); is_chain(Y)|] ==> \
 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
  (fn prems =>
         [

         (atac 1)
         ]);
 
 
 qed_goal "diag_lubMF2_1" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \  is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
  (fn prems =>
         [

         (etac ch2ch_MF2L 1),
         (atac 1)
         ]);
 
 qed_goal "diag_lubMF2_2" thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+"[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
 \  is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
  (fn prems =>
         [

         (rtac ex_lubMF2 1),
         (REPEAT (atac 1)),
         (etac diag_lubMF2_1 1),
         (REPEAT (atac 1))
         ]);
-
-
 
 
 (* ------------------------------------------------------------------------ *)
 (* The following results are about a curried function that is continuous    *)
 (* in both arguments                                                        *)

         (rtac 
         ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1),
         (atac 1)
         ]);
 
-
 (* ------------------------------------------------------------------------ *)
 (* What D.A.Schmidt calls continuity of abstraction                         *)
 (* never used here                                                          *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_abstraction" thy
-"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a=>'b=>'c) x y)|] ==>\
+"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
 \ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac trans 1),

         (rtac (cont2contlub RS contlubE RS spec RS mp RS sym) 1),
         (etac spec 1),
         (atac 1)
         ]);
 
-
 qed_goal "mono2mono_app" thy 
 "[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
 \        monofun(%x.(ft(x))(tt(x)))"
  (fn prems =>
         [