domain package:
* theorems are stored in the theory
* creates hierachical name space
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
* separator between mutual domain definitions changed from "," to "and"
* minor debugging of Domain_Library.mk_var_names
(* Title: HOLCF/lift3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of ('a)u for class pcpo
*)
Lift3 = Lift2 +
arities "u" :: (pcpo)pcpo (* Witness lift2.ML *)
consts
up :: "'a -> ('a)u"
lift :: "('a->'c)-> ('a)u -> 'c"
rules
inst_lift_pcpo "UU::('a)u = UU_lift"
up_def "up == (LAM x.Iup(x))"
lift_def "lift == (LAM f p.Ilift(f)(p))"
end