src/HOLCF/Lift1.thy
author paulson
Tue, 05 Sep 2000 10:16:03 +0200
changeset 9841 ca3173f87b5c
parent 5192 704dd3a6d47d
permissions -rw-r--r--
safe_meson_tac -> meson_tac

(*  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