# HG changeset patch
# User slotosch
# Date 864551272 -7200
# Node ID 194ae2e0c1938fc064d2e9ecf8800b880109605d
# Parent  bc4d107fb6dd3dcfe81375509fefe5550cb1ddbd
eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
        minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and     dist_eqI (in domain-package)
added instances
instance fun  :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*"  :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord

diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Cfun1.ML
--- a/src/HOLCF/Cfun1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cfun1.ML	Sun May 25 11:07:52 1997 +0200
@@ -35,14 +35,14 @@
 (* less_cfun is a partial order on type 'a -> 'b                            *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "refl_less_cfun" thy [less_cfun_def] "less(f::'a->'b) f"
+qed_goalw "refl_less_cfun" thy [less_cfun_def] "(f::'a->'b) << f"
 (fn prems =>
         [
         (rtac refl_less 1)
         ]);
 
 qed_goalw "antisym_less_cfun" thy [less_cfun_def] 
-        "[|less (f1::'a->'b) f2; less f2 f1|] ==> f1 = f2"
+        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -55,7 +55,7 @@
         ]);
 
 qed_goalw "trans_less_cfun" thy [less_cfun_def] 
-        "[|less (f1::'a->'b) f2; less f2 f3|] ==> less f1 f3"
+        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cfun1.thy	Sun May 25 11:07:52 1997 +0200
@@ -13,6 +13,9 @@
 
 typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
 
+(* to make << defineable *)
+instance "->"  :: (cpo,cpo)sq_ord
+
 consts  
         fapp      :: "('a -> 'b)=>('a => 'b)"   (* usually Rep_Cfun *)
                                                 (* application      *)
@@ -33,6 +36,6 @@
   fabs_def	"fabs==Abs_CFun"
   fapp_def	"fapp==Rep_CFun"
 
-  less_cfun_def "less == (% fo1 fo2. fapp fo1 << fapp fo2 )"
+  less_cfun_def "(op <<) == (% fo1 fo2. fapp fo1 << fapp fo2 )"
 
 end
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cfun2.ML	Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
 qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
  (fn prems => 
         [
-	(fold_goals_tac [po_def,less_cfun_def]),
+	(fold_goals_tac [less_cfun_def]),
 	(rtac refl 1)
         ]);
 
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cont.thy	Sun May 25 11:07:52 1997 +0200
@@ -11,7 +11,7 @@
 (* 
 
    Now we change the default class! Form now on all untyped typevariables are
-   of default class pcpo
+   of default class po
 
 *)
 
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Cprod1.ML
--- a/src/HOLCF/Cprod1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cprod1.ML	Sun May 25 11:07:52 1997 +0200
@@ -24,11 +24,11 @@
         (Asm_simp_tac 1)
         ]);
 
-qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less (p::'a*'b) p"
+qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "(p::'a*'b) << p"
  (fn prems => [Simp_tac 1]);
 
 qed_goalw "antisym_less_cprod" thy [less_cprod_def]
-        "[|less (p1::'a * 'b) p2;less p2 p1|] ==> p1=p2"
+        "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -38,7 +38,7 @@
         ]);
 
 qed_goalw "trans_less_cprod" thy [less_cprod_def]
-        "[|less (p1::'a*'b) p2;less p2 p3|] ==> less p1 p3"
+        "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Cprod1.thy
--- a/src/HOLCF/Cprod1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cprod1.thy	Sun May 25 11:07:52 1997 +0200
@@ -12,8 +12,10 @@
 
 default cpo
 
+instance "*"::(sq_ord,sq_ord)sq_ord 
+
 defs
 
-  less_cprod_def "less p1 p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
+  less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
 
 end
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Cprod2.ML
--- a/src/HOLCF/Cprod2.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Cprod2.ML	Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
 qed_goal "inst_cprod_po" thy "(op <<)=(%x y.fst x<<fst y & snd x<<snd y)"
  (fn prems => 
         [
-        (fold_goals_tac [po_def,less_cprod_def]),
+        (fold_goals_tac [less_cprod_def]),
         (rtac refl 1)
         ]);
 
@@ -71,7 +71,7 @@
         (asm_simp_tac (!simpset addsimps [inst_cprod_po]) 1)
         ]);
 
-qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
+qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Discrete0.ML
--- a/src/HOLCF/Discrete0.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Discrete0.ML	Sun May 25 11:07:52 1997 +0200
@@ -6,17 +6,17 @@
 Proves that 'a discr is a po
 *)
 
-goalw thy [less_discr_def] "less (x::('a::term)discr) x";
+goalw thy [less_discr_def] "(x::('a::term)discr) << x";
 by (rtac refl 1);
 qed "less_discr_refl";
 
 goalw thy [less_discr_def]
-  "!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
+  "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x <<  z";
 by (etac trans 1);
 by (assume_tac 1);
 qed "less_discr_trans";
 
 goalw thy [less_discr_def]
-  "!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
+  "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";
 by (assume_tac 1);
 qed "less_discr_antisym";
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Discrete0.thy
--- a/src/HOLCF/Discrete0.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Discrete0.thy	Sun May 25 11:07:52 1997 +0200
@@ -10,7 +10,9 @@
 
 datatype 'a discr = Discr 'a
 
+instance discr :: (term)sq_ord
+
 defs
-less_discr_def "(less::('a::term)discr=>'a discr=>bool)  ==  op ="
+less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool)  ==  op ="
 
 end
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Discrete1.ML
--- a/src/HOLCF/Discrete1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Discrete1.ML	Sun May 25 11:07:52 1997 +0200
@@ -6,7 +6,7 @@
 Proves that 'a discr is a cpo
 *)
 
-goalw thy [po_def,less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
+goalw thy [less_discr_def] "((x::('a::term)discr) << y) = (x=y)";
 by (rtac refl 1);
 qed "discr_less_eq";
 AddIffs [discr_less_eq];
@@ -14,7 +14,7 @@
 goalw thy [is_chain]
  "!!S::nat=>('a::term)discr. is_chain S ==> S i = S 0";
 by (nat_ind_tac "i" 1);
- by (rtac refl 1);
+by (rtac refl 1);
 by (etac subst 1);
 by (rtac sym 1);
 by (Fast_tac 1);
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Fun1.ML
--- a/src/HOLCF/Fun1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Fun1.ML	Sun May 25 11:07:52 1997 +0200
@@ -12,14 +12,14 @@
 (* less_fun is a partial order on 'a => 'b                                  *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "refl_less_fun" thy [less_fun_def] "less(f::'a::term =>'b::po) f"
+qed_goalw "refl_less_fun" thy [less_fun_def] "(f::'a::term =>'b::po) << f"
 (fn prems =>
         [
         (fast_tac (HOL_cs addSIs [refl_less]) 1)
         ]);
 
 qed_goalw "antisym_less_fun" Fun1.thy [less_fun_def] 
-        "[|less (f1::'a::term =>'b::po) f2; less f2 f1|] ==> f1 = f2"
+        "[|(f1::'a::term =>'b::po) << f2; f2 << f1|] ==> f1 = f2"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -28,7 +28,7 @@
         ]);
 
 qed_goalw "trans_less_fun" Fun1.thy [less_fun_def] 
-        "[|less (f1::'a::term =>'b::po) f2; less f2 f3 |] ==> less f1 f3"
+        "[|(f1::'a::term =>'b::po) << f2; f2 << f3 |] ==> f1 << f3"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Fun1.thy
--- a/src/HOLCF/Fun1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Fun1.thy	Sun May 25 11:07:52 1997 +0200
@@ -12,14 +12,11 @@
 
 Fun1 = Pcpo +
 
-(* default class is still term *)
+(* to make << defineable: *)
+instance fun  :: (term,sq_ord)sq_ord
 
 defs
-   (* definition of the ordering less_fun            *)
-   (* in fun1.ML it is proved that less_fun is a po *)
-   
-  less_fun_def "less == (%f1 f2.!x. f1 x << f2 x)"  
-
+  less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"  
 end
 
 
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Fun2.ML	Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
 qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)"
  (fn prems => 
         [
-	(fold_goals_tac [po_def,less_fun_def]),
+	(fold_goals_tac [less_fun_def]),
 	(rtac refl 1)
         ]);
 
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Lift1.ML
--- a/src/HOLCF/Lift1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Lift1.ML	Sun May 25 11:07:52 1997 +0200
@@ -13,18 +13,18 @@
 (* less_lift is a partial order on type 'a -> 'b                            *)
 (* ------------------------------------------------------------------------ *)
 
-goalw thy [less_lift_def] "less (x::'a lift) x";
+goalw thy [less_lift_def] "(x::'a lift) << x";
 by (fast_tac HOL_cs 1);
 qed"refl_less_lift";
 
 val prems = goalw thy [less_lift_def] 
-  "[|less (x1::'a lift) x2; less x2 x1|] ==> x1 = x2";
+  "[|(x1::'a lift) << x2; x2 << x1|] ==> x1 = x2";
 by (cut_facts_tac prems 1);
 by (fast_tac HOL_cs 1);
 qed"antisym_less_lift";
 
 val prems = goalw Lift1.thy [less_lift_def] 
-  "[|less (x1::'a lift) x2; less x2 x3|] ==> less x1 x3";
+  "[|(x1::'a lift) << x2; x2 << x3|] ==> x1 << x3";
 by (cut_facts_tac prems 1);
 by (fast_tac HOL_cs 1);
 qed"trans_less_lift";
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Lift1.thy
--- a/src/HOLCF/Lift1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Lift1.thy	Sun May 25 11:07:52 1997 +0200
@@ -12,8 +12,9 @@
 
 datatype 'a lift = Undef | Def 'a
 
+instance lift :: (term)sq_ord
 defs 
  
- less_lift_def  "less x y == (x=y | x=Undef)"
+ less_lift_def  "x << y == (x=y | x=Undef)"
 
 end
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Lift2.ML
--- a/src/HOLCF/Lift2.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Lift2.ML	Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
 qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
  (fn prems => 
         [
-        (fold_goals_tac [po_def,less_lift_def]),
+        (fold_goals_tac [less_lift_def]),
         (rtac refl 1)
         ]);
 
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Pcpo.ML	Sun May 25 11:07:52 1997 +0200
@@ -195,7 +195,7 @@
         (resolve_tac prems 1)
         ]);
 
-qed_goal "not_less2not_eq" thy "~x<<y ==> ~x=y"
+qed_goal "not_less2not_eq" thy "~(x::'a::po)<<y ==> ~x=y"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Porder0.ML
--- a/src/HOLCF/Porder0.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Porder0.ML	Sun May 25 11:07:52 1997 +0200
@@ -7,30 +7,12 @@
 
 open Porder0;
 
-qed_goalw "refl_less" thy [ po_def ] "x << x"
-(fn prems =>
-        [
-        (fast_tac (HOL_cs addSIs [ax_refl_less]) 1)
-        ]);
-
 AddIffs [refl_less];
 
-qed_goalw "antisym_less" thy [ po_def ] "[| x << y; y << x |] ==> x = y"
-(fn prems =>
-        [
-        (fast_tac (HOL_cs addSIs prems@[ax_antisym_less]) 1)
-        ]);
-
-qed_goalw "trans_less" thy [ po_def ] "[| x << y; y << z |] ==> x << z"
-(fn prems =>
-        [
-        (fast_tac (HOL_cs addIs prems@[ax_trans_less]) 1)
-        ]);
-
 (* ------------------------------------------------------------------------ *)
 (* minimal fixes least element                                              *)
 (* ------------------------------------------------------------------------ *)
-bind_thm("minimal2UU",allI RS (prove_goal thy "!x.uu<<x==>uu=(@u.!y.u<<y)"
+bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po.uu<<x==>uu=(@u.!y.u<<y)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -45,7 +27,7 @@
 (* the reverse law of anti--symmetrie of <<                                 *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x"
+qed_goal "antisym_less_inverse" thy "(x::'a::po)=y ==> x << y & y << x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -56,7 +38,7 @@
 
 
 qed_goal "box_less" thy
-"[| a << b; c << a; b << d|] ==> c << d"
+"[| (a::'a::po) << b; c << a; b << d|] ==> c << d"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Porder0.thy	Sun May 25 11:07:52 1997 +0200
@@ -9,25 +9,22 @@
 
 Porder0 = Arith +
 
-(* first the global constant for HOLCF type classes *)
-consts
-  less        :: "['a,'a] => bool"
+	(* introduce a (syntactic) class for the constant << *)
+axclass sq_ord<term
 
-axclass po < term
-        (* class axioms: *)
-ax_refl_less       "less x x"        
-ax_antisym_less    "[|less x y; less y x |] ==> x = y"    
-ax_trans_less      "[|less x y; less y z |] ==> less x z"
- 
-	(* characteristic constant << on po *)
+	(* characteristic constant << for po *)
 consts
-  "<<"          :: "['a,'a::po] => bool"        (infixl 55)
+  "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)
 
 syntax (symbols)
-  "op <<"       :: "['a,'a::po] => bool"        (infixl "\\<sqsubseteq>" 55)
+  "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\\<sqsubseteq>" 55)
 
-defs
-po_def             "(op <<) == less"
+axclass po < sq_ord
+        (* class axioms: *)
+refl_less       "x << x"        
+antisym_less    "[|x << y; y << x |] ==> x = y"    
+trans_less      "[|x << y; y << z |] ==> x << z"
+ 
 end 
 
 
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Sprod1.ML
--- a/src/HOLCF/Sprod1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Sprod1.ML	Sun May 25 11:07:52 1997 +0200
@@ -12,11 +12,11 @@
 (* less_sprod is a partial order on Sprod                                   *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "refl_less_sprod" thy [less_sprod_def]"less (p::'a ** 'b) p"
+qed_goalw "refl_less_sprod" thy [less_sprod_def]"(p::'a ** 'b) << p"
 (fn prems => [(fast_tac (HOL_cs addIs [refl_less]) 1)]);
 
 qed_goalw "antisym_less_sprod" thy [less_sprod_def]
-        "[|less (p1::'a ** 'b) p2;less p2 p1|] ==> p1=p2"
+        "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -26,7 +26,7 @@
         ]);
 
 qed_goalw "trans_less_sprod" thy [less_sprod_def]
-        "[|less (p1::'a**'b) p2;less p2 p3|] ==> less p1 p3"
+        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Sprod1.thy
--- a/src/HOLCF/Sprod1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Sprod1.thy	Sun May 25 11:07:52 1997 +0200
@@ -8,7 +8,9 @@
 
 Sprod1 = Sprod0 +
 
+instance "**"::(sq_ord,sq_ord)sq_ord 
+
 defs
-  less_sprod_def "less p1 p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
+  less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
 
 end
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Sprod2.ML
--- a/src/HOLCF/Sprod2.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Sprod2.ML	Sun May 25 11:07:52 1997 +0200
@@ -12,7 +12,7 @@
 qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
  (fn prems => 
         [
-	(fold_goals_tac [po_def,less_sprod_def]),
+	(fold_goals_tac [less_sprod_def]),
 	(rtac refl 1)
         ]);
 
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Ssum1.ML
--- a/src/HOLCF/Ssum1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Ssum1.ML	Sun May 25 11:07:52 1997 +0200
@@ -41,7 +41,7 @@
 in
 
 val less_ssum1a = prove_goalw thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> less s1 s2 = (x << y)"
+"[|s1=Isinl(x::'a); s2=Isinl(y::'a)|] ==> s1 << s2 = (x << y)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -82,7 +82,7 @@
 
 
 val less_ssum1b = prove_goalw thy [less_ssum_def]
-"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> less s1 s2 = (x << y)"
+"[|s1=Isinr(x::'b); s2=Isinr(y::'b)|] ==> s1 << s2 = (x << y)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -124,7 +124,7 @@
 
 
 val less_ssum1c = prove_goalw thy [less_ssum_def]
-"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> less s1 s2 = ((x::'a) = UU)"
+"[|s1=Isinl(x::'a); s2=Isinr(y::'b)|] ==> s1 << s2 = ((x::'a) = UU)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -166,7 +166,7 @@
 
 
 val less_ssum1d = prove_goalw thy [less_ssum_def]
-"[|s1=Isinr(x); s2=Isinl(y)|] ==> less s1 s2 = (x = UU)"
+"[|s1=Isinr(x); s2=Isinl(y)|] ==> s1 << s2 = (x = UU)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -213,7 +213,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "less_ssum2a" thy 
-        "less (Isinl x) (Isinl y) = (x << y)"
+        "(Isinl x) << (Isinl y) = (x << y)"
  (fn prems =>
         [
         (rtac less_ssum1a 1),
@@ -222,7 +222,7 @@
         ]);
 
 qed_goal "less_ssum2b" thy 
-        "less (Isinr x) (Isinr y) = (x << y)"
+        "(Isinr x) << (Isinr y) = (x << y)"
  (fn prems =>
         [
         (rtac less_ssum1b 1),
@@ -231,7 +231,7 @@
         ]);
 
 qed_goal "less_ssum2c" thy 
-        "less (Isinl x) (Isinr y) = (x = UU)"
+        "(Isinl x) << (Isinr y) = (x = UU)"
  (fn prems =>
         [
         (rtac less_ssum1c 1),
@@ -240,7 +240,7 @@
         ]);
 
 qed_goal "less_ssum2d" thy 
-        "less (Isinr x) (Isinl y) = (x = UU)"
+        "(Isinr x) << (Isinl y) = (x = UU)"
  (fn prems =>
         [
         (rtac less_ssum1d 1),
@@ -253,7 +253,7 @@
 (* less_ssum is a partial order on ++                                     *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "refl_less_ssum" thy "less (p::'a++'b) p"
+qed_goal "refl_less_ssum" thy "(p::'a++'b) << p"
  (fn prems =>
         [
         (res_inst_tac [("p","p")] IssumE2 1),
@@ -266,7 +266,7 @@
         ]);
 
 qed_goal "antisym_less_ssum" thy 
- "[|less (p1::'a++'b) p2; less p2 p1|] ==> p1=p2"
+ "[|(p1::'a++'b) << p2; p2 << p1|] ==> p1=p2"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -296,7 +296,7 @@
         ]);
 
 qed_goal "trans_less_ssum" thy 
- "[|less (p1::'a++'b) p2; less p2 p3|] ==> less p1 p3"
+ "[|(p1::'a++'b) << p2; p2 << p3|] ==> p1 << p3"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Ssum1.thy
--- a/src/HOLCF/Ssum1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Ssum1.thy	Sun May 25 11:07:52 1997 +0200
@@ -8,8 +8,10 @@
 
 Ssum1 = Ssum0 +
 
+instance "++"::(pcpo,pcpo)sq_ord
+
 defs
-  less_ssum_def "less == (%s1 s2.@z.
+  less_ssum_def "(op <<) == (%s1 s2.@z.
          (! u x.s1=Isinl u & s2=Isinl x --> z = u << x)
         &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)
         &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Ssum2.ML
--- a/src/HOLCF/Ssum2.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Ssum2.ML	Sun May 25 11:07:52 1997 +0200
@@ -16,7 +16,7 @@
 \        &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
  (fn prems => 
         [
-        (fold_goals_tac [po_def,less_ssum_def]),
+        (fold_goals_tac [less_ssum_def]),
         (rtac refl 1)
         ]);
 
@@ -27,25 +27,25 @@
 qed_goal "less_ssum3a" thy "Isinl x << Isinl y = x << y"
  (fn prems =>
         [
-        (simp_tac (!simpset addsimps [po_def,less_ssum2a]) 1)
+        (simp_tac (!simpset addsimps [less_ssum2a]) 1)
         ]);
 
 qed_goal "less_ssum3b" thy "Isinr x << Isinr y = x << y"
  (fn prems =>
         [
-        (simp_tac (!simpset addsimps [po_def,less_ssum2b]) 1)
+        (simp_tac (!simpset addsimps [less_ssum2b]) 1)
         ]);
 
 qed_goal "less_ssum3c" thy "Isinl x << Isinr y = (x = UU)"
  (fn prems =>
         [
-        (simp_tac (!simpset addsimps [po_def,less_ssum2c]) 1)
+        (simp_tac (!simpset addsimps [less_ssum2c]) 1)
         ]);
 
 qed_goal "less_ssum3d" thy "Isinr x << Isinl y = (x = UU)"
  (fn prems =>
         [
-        (simp_tac (!simpset addsimps [po_def,less_ssum2d]) 1)
+        (simp_tac (!simpset addsimps [less_ssum2d]) 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Up1.ML
--- a/src/HOLCF/Up1.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Up1.ML	Sun May 25 11:07:52 1997 +0200
@@ -93,7 +93,7 @@
 val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2];
 
 qed_goalw "less_up1a"  thy [less_up_def]
-        "less(Abs_Up(Inl ()))(z)"
+        "Abs_Up(Inl ())<< z"
  (fn prems =>
         [
         (stac Abs_Up_inverse2 1),
@@ -102,7 +102,7 @@
         ]);
 
 qed_goalw "less_up1b" thy [Iup_def,less_up_def]
-        "~less (Iup x) (Abs_Up(Inl ()))"
+        "~(Iup x) << (Abs_Up(Inl ()))"
  (fn prems =>
         [
         (rtac notI 1),
@@ -116,7 +116,7 @@
         ]);
 
 qed_goalw "less_up1c"  thy [Iup_def,less_up_def]
-        "less (Iup x) (Iup y)=(x<<y)"
+        " (Iup x) << (Iup y)=(x<<y)"
  (fn prems =>
         [
         (stac Abs_Up_inverse2 1),
@@ -127,7 +127,7 @@
         ]);
 
 
-qed_goal "refl_less_up"  thy "less (p::'a u) p"
+qed_goal "refl_less_up"  thy "(p::'a u) << p"
  (fn prems =>
         [
         (res_inst_tac [("p","p")] upE 1),
@@ -139,7 +139,7 @@
         ]);
 
 qed_goal "antisym_less_up"  thy 
-        "!!p1.[|less(p1::'a u) p2;less p2 p1|] ==> p1=p2"
+        "!!p1.[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
  (fn _ =>
         [
         (res_inst_tac [("p","p1")] upE 1),
@@ -147,13 +147,13 @@
         (res_inst_tac [("p","p2")] upE 1),
         (etac sym 1),
         (hyp_subst_tac 1),
-        (res_inst_tac [("P","less (Iup x) (Abs_Up(Inl ()))")] notE 1),
+        (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
         (rtac less_up1b 1),
         (atac 1),
         (hyp_subst_tac 1),
         (res_inst_tac [("p","p2")] upE 1),
         (hyp_subst_tac 1),
-        (res_inst_tac [("P","less (Iup x) (Abs_Up(Inl ()))")] notE 1),
+        (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
         (rtac less_up1b 1),
         (atac 1),
         (hyp_subst_tac 1),
@@ -164,7 +164,7 @@
         ]);
 
 qed_goal "trans_less_up"  thy 
-        "[|less (p1::'a u) p2;less p2 p3|] ==> less p1 p3"
+        "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Up1.thy
--- a/src/HOLCF/Up1.thy	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Up1.thy	Sun May 25 11:07:52 1997 +0200
@@ -14,6 +14,8 @@
 
 typedef (Up) ('a) "u" = "{x::(unit + 'a).True}"
 
+instance u :: (sq_ord)sq_ord
+
 consts
   Iup         :: "'a => ('a)u"
   Ifup        :: "('a->'b)=>('a)u => 'b"
@@ -21,7 +23,7 @@
 defs
   Iup_def     "Iup x == Abs_Up(Inr(x))"
   Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
-  less_up_def "less == (%x1 x2.case Rep_Up(x1) of                 
+  less_up_def "(op <<) == (%x1 x2.case Rep_Up(x1) of                 
                Inl(y1) => True          
              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
                                             | Inr(z2) => y2<<z2))"
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Up2.ML
--- a/src/HOLCF/Up2.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Up2.ML	Sun May 25 11:07:52 1997 +0200
@@ -15,7 +15,7 @@
 \                                            | Inr(z2) => y2<<z2))"
  (fn prems => 
         [
-        (fold_goals_tac [po_def,less_up_def]),
+        (fold_goals_tac [less_up_def]),
         (rtac refl 1)
         ]);
 
@@ -26,7 +26,7 @@
 qed_goal "minimal_up" thy "Abs_Up(Inl ()) << z"
  (fn prems =>
         [
-        (simp_tac (!simpset addsimps [po_def,less_up1a]) 1)
+        (simp_tac (!simpset addsimps [less_up1a]) 1)
         ]);
 
 bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
@@ -45,13 +45,13 @@
 qed_goal "less_up2b" thy "~ Iup(x) << Abs_Up(Inl ())"
  (fn prems =>
         [
-        (simp_tac (!simpset addsimps [po_def,less_up1b]) 1)
+        (simp_tac (!simpset addsimps [less_up1b]) 1)
         ]);
 
 qed_goal "less_up2c" thy "(Iup(x)<<Iup(y)) = (x<<y)"
  (fn prems =>
         [
-        (simp_tac (!simpset addsimps [po_def,less_up1c]) 1)
+        (simp_tac (!simpset addsimps [less_up1c]) 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/domain/theorems.ML	Sun May 25 11:07:52 1997 +0200
@@ -51,7 +51,7 @@
                                 cut_facts_tac prems 1,
                                 fast_tac HOL_cs 1]);
 
-val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
+val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
                                 rtac rev_contrapos 1,
                                 etac (antisym_less_inverse RS conjunct1) 1,
                                 resolve_tac prems 1]);