changeset 2640 | ee4dfce170a0 |
parent 2278 | d63ffafce255 |
child 12030 | 46d57d0290a2 |
--- a/src/HOLCF/Up2.thy Sat Feb 15 18:24:05 1997 +0100 +++ b/src/HOLCF/Up2.thy Mon Feb 17 10:57:11 1997 +0100 @@ -9,15 +9,7 @@ Up2 = Up1 + -(* Witness for the above arity axiom is up1.ML *) - -arities "u" :: (pcpo)po - -rules - -(* instance of << for type ('a)u *) - -inst_up_po "((op <<)::[('a)u,('a)u]=>bool) = less_up" +instance u :: (pcpo)po (refl_less_up,antisym_less_up,trans_less_up) end