(* Title: HOLCF/Lift1.thy ID: $Id$ Author: Olaf Mueller, Robert Sandner Copyright 1996 Technische Universitaet MuenchenLifting types of class term to flat pcpo's*)Lift1 = ccc1 + default termdatatype 'a lift = Undef | Def 'adefs less_lift_def "less x y == (x=y | x=Undef)"end