src/HOLCF/Lift2.thy

Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy

Lift2 = Lift1 + 

default term

arities "lift" :: (term)po

rules

 inst_lift_po   "((op <<)::['a lift,'a lift]=>bool) = less_lift"

end