src/HOLCF/Pcpo.ML

         (rtac least 1)]);
 
 bind_thm("minimal",UU_least RS spec);
 
 (* ------------------------------------------------------------------------ *)
-(* in pcpo's everthing equal to THE lub has lub properties for every chain  *)
+(* in cpo's everthing equal to THE lub has lub properties for every chain  *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "thelubE"  thy 
-        "[| is_chain(S);lub(range(S)) = (l::'a::pcpo)|] ==> range(S) <<| l "
+        "[| is_chain(S);lub(range(S)) = (l::'a::cpo)|] ==> range(S) <<| l "
 (fn prems =>
         [
         (cut_facts_tac prems 1), 
         (hyp_subst_tac 1),
         (rtac lubI 1),

 
 bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub);
 (* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1        *)
 
 qed_goal "maxinch_is_thelub" thy "is_chain Y ==> \
-\       max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::pcpo))" 
+\       max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))" 
 (fn prems => 
         [
         cut_facts_tac prems 1,
         rtac iffI 1,
         fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1,

 (* ------------------------------------------------------------------------ *)
 (* the << relation between two chains is preserved by their lubs            *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_mono" thy 
-        "[|is_chain(C1::(nat=>'a::pcpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
+        "[|is_chain(C1::(nat=>'a::cpo));is_chain(C2); ! k. C1(k) << C2(k)|]\
 \           ==> lub(range(C1)) << lub(range(C2))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (etac is_lub_thelub 1),

 (* ------------------------------------------------------------------------ *)
 (* the = relation between two chains is preserved by their lubs            *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_equal" thy
-"[| is_chain(C1::(nat=>'a::pcpo));is_chain(C2);!k.C1(k)=C2(k)|]\
+"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k.C1(k)=C2(k)|]\
 \       ==> lub(range(C1))=lub(range(C2))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac antisym_less 1),

 (* ------------------------------------------------------------------------ *)
 (* more results about mono and = of lubs of chains                          *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_mono2" thy 
-"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
+"[|? j.!i. j<i --> X(i::nat)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
 \ ==> lub(range(X))<<lub(range(Y))"
  (fn prems =>
         [
         (rtac  exE 1),
         (resolve_tac prems 1),

         (rtac is_ub_thelub 1),
         (resolve_tac prems 1)
         ]);
 
 qed_goal "lub_equal2" thy 
-"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::pcpo);is_chain(Y)|]\
+"[|? j.!i. j<i --> X(i)=Y(i);is_chain(X::nat=>'a::cpo);is_chain(Y)|]\
 \ ==> lub(range(X))=lub(range(Y))"
  (fn prems =>
         [
         (rtac antisym_less 1),
         (rtac lub_mono2 1),

         (safe_tac HOL_cs),
         (rtac sym 1),
         (fast_tac HOL_cs 1)
         ]);
 
-qed_goal "lub_mono3" thy "[|is_chain(Y::nat=>'a::pcpo);is_chain(X);\
+qed_goal "lub_mono3" thy "[|is_chain(Y::nat=>'a::cpo);is_chain(X);\
 \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac is_lub_thelub 1),