src/HOLCF/Up3.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3842 b55686a7b22c
child 10834 a7897aebbffc
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/Up3.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 
     7 Class instance of  ('a)u for class pcpo
     8 
     9 *)
    10 
    11 Up3 = Up2 +
    12 
    13 instance u :: (pcpo)pcpo      (least_up,cpo_up)
    14 
    15 constdefs  
    16         up  :: "'a -> ('a)u"
    17        "up  == (LAM x. Iup(x))"
    18         fup :: "('a->'c)-> ('a)u -> 'c"
    19        "fup == (LAM f p. Ifup(f)(p))"
    20 
    21 translations
    22 "case l of up`x => t1" == "fup`(LAM x. t1)`l"
    23 
    24 end
    25 
    26 
    27