author | wenzelm |
Mon, 09 Dec 1996 16:41:04 +0100 | |
changeset 2348 | b51e104ecf40 |
parent 2278 | d63ffafce255 |
child 2640 | ee4dfce170a0 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Up2.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Class Instance u::(pcpo)po *) 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" end