| author | clasohm |
| Tue, 24 Oct 1995 13:40:06 +0100 | |
| changeset 1289 | 2edd7a39d92a |
| parent 442 | 13ac1fd0a14d |
| child 1479 | 21eb5e156d91 |
| permissions | -rw-r--r-- |
(* Title: HOLCF/lift2.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Class Instance u::(pcpo)po *) Lift2 = Lift1 + (* Witness for the above arity axiom is lift1.ML *) arities "u" :: (pcpo)po rules (* instance of << for type ('a)u *) inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift" end