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))"