src/HOLCF/Up1.thy
changeset 3842 b55686a7b22c
parent 3323 194ae2e0c193
child 6543 da7b170fc8a7
--- a/src/HOLCF/Up1.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up1.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -23,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 "(op <<) == (%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))"