| author | wenzelm |
| Sat, 10 Jul 1999 21:46:15 +0200 | |
| changeset 6967 | a3c163ed1e04 |
| parent 5192 | 704dd3a6d47d |
| permissions | -rw-r--r-- |
(* Title: HOLCF/Lift1.thy ID: $Id$ Author: Olaf Mueller Copyright 1996 Technische Universitaet Muenchen Lifting types of class term to flat pcpo's *) Lift1 = Cprod3 + Datatype + default term datatype 'a lift = Undef | Def 'a instance lift :: (term)sq_ord defs less_lift_def "x << y == (x=y | x=Undef)" end