src/HOLCF/Up1.thy

 
 (* new type for lifting *)
 
 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"
 
 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))"
 end