author | huffman |
Wed, 02 Mar 2005 22:57:08 +0100 | |
changeset 15563 | 9e125b675253 |
parent 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Up3.thy ID: $Id$ Author: Franz Regensburger 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