- Installed specific code generator for equality enforcing that
arguments do not have function types, which would result in
an error message during compilation.
- Added test case generators for basic types.
(* Title: HOLCF/Up3.thy
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ('a)u for class pcpo
*)
Up3 = Up2 +
instance u :: (pcpo)pcpo (least_up,cpo_up)
constdefs
up :: "'a -> ('a)u"
"up == (LAM x. Iup(x))"
fup :: "('a->'c)-> ('a)u -> 'c"
"fup == (LAM f p. Ifup(f)(p))"
translations
"case l of up$x => t1" == "fup$(LAM x. t1)$l"
end