author | wenzelm |
Tue, 20 May 1997 19:29:50 +0200 | |
changeset 3257 | 4e3724e0659f |
parent 2640 | ee4dfce170a0 |
child 3842 | b55686a7b22c |
permissions | -rw-r--r-- |
(* 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