src/HOLCF/Up3.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 3842 b55686a7b22c
child 10834 a7897aebbffc
permissions -rw-r--r--
made tutorial first;
     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