| changeset 243 | c22b85994e17 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/lift2.thy Wed Jan 19 17:35:01 1994 +0100 @@ -0,0 +1,25 @@ +(* 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 + + +