Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Up3.thy
author wenzelm
Tue, 27 Jul 1999 22:04:30 +0200
changeset 7108 0229ce6735f6
parent 3842 b55686a7b22c
child 10834 a7897aebbffc
permissions -rw-r--r--
fixed comment;

(*  Title:      HOLCF/Up3.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen


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
isabelle