src/HOLCF/Ssum1.ML

         THEN (etac sym 1))
 
 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),
         (rtac  select_equality 1),
         (dtac conjunct1 2),

         (Simp_tac 1)
         ]);
 
 
 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),
         (rtac  select_equality 1),
         (dtac conjunct2 2),

         (rtac refl_less 1)
         ]);
 
 
 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),
         (rtac  select_equality 1),
         (rtac conjI 1),

         (fast_tac HOL_cs 1)
         ]);
 
 
 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),
         (rtac  select_equality 1),
         (dtac conjunct2 2),

 (* ------------------------------------------------------------------------ *)
 (* optimize lemmas about less_ssum                                          *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "less_ssum2a" thy 
-        "less (Isinl x) (Isinl y) = (x << y)"
+        "(Isinl x) << (Isinl y) = (x << y)"
  (fn prems =>
         [
         (rtac less_ssum1a 1),
         (rtac refl 1),
         (rtac refl 1)
         ]);
 
 qed_goal "less_ssum2b" thy 
-        "less (Isinr x) (Isinr y) = (x << y)"
+        "(Isinr x) << (Isinr y) = (x << y)"
  (fn prems =>
         [
         (rtac less_ssum1b 1),
         (rtac refl 1),
         (rtac refl 1)
         ]);
 
 qed_goal "less_ssum2c" thy 
-        "less (Isinl x) (Isinr y) = (x = UU)"
+        "(Isinl x) << (Isinr y) = (x = UU)"
  (fn prems =>
         [
         (rtac less_ssum1c 1),
         (rtac refl 1),
         (rtac refl 1)
         ]);
 
 qed_goal "less_ssum2d" thy 
-        "less (Isinr x) (Isinl y) = (x = UU)"
+        "(Isinr x) << (Isinl y) = (x = UU)"
  (fn prems =>
         [
         (rtac less_ssum1d 1),
         (rtac refl 1),
         (rtac refl 1)

 
 (* ------------------------------------------------------------------------ *)
 (* 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),
         (hyp_subst_tac 1),
         (rtac (less_ssum2a RS iffD2) 1),

         (rtac (less_ssum2b RS iffD2) 1),
         (rtac refl_less 1)
         ]);
 
 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),
         (res_inst_tac [("p","p1")] IssumE2 1),
         (hyp_subst_tac 1),

         (etac (less_ssum2b RS iffD1) 1),
         (etac (less_ssum2b RS iffD1) 1)
         ]);
 
 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),
         (res_inst_tac [("p","p1")] IssumE2 1),
         (hyp_subst_tac 1),