author | paulson |
Wed, 23 Apr 1997 11:00:48 +0200 | |
changeset 3017 | 84c2178db936 |
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