isabelle: src/HOLCF/Up3.thy@9e85d2b04867 (annotated)

2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	1	(* Title: HOLCF/Up3.thy
d63ffafce255 * empty log message * oheimb parents: diff changeset	2	ID: $Id$
d63ffafce255 * empty log message * oheimb parents: diff changeset	3	Author: Franz Regensburger
d63ffafce255 * empty log message * oheimb parents: diff changeset	4
d63ffafce255 * empty log message * oheimb parents: diff changeset	5	Class instance of ('a)u for class pcpo
d63ffafce255 * empty log message * oheimb parents: diff changeset	6	*)
d63ffafce255 * empty log message * oheimb parents: diff changeset	7
d63ffafce255 * empty log message * oheimb parents: diff changeset	8	Up3 = Up2 +
d63ffafce255 * empty log message * oheimb parents: diff changeset	9
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	10	instance u :: (pcpo)pcpo (least_up,cpo_up)
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	11
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	12	constdefs
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	13	up :: "'a -> ('a)u"
3842 b55686a7b22c fixed dots; wenzelm parents: 2640 diff changeset	14	"up == (LAM x. Iup(x))"
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	15	fup :: "('a->'c)-> ('a)u -> 'c"
3842 b55686a7b22c fixed dots; wenzelm parents: 2640 diff changeset	16	"fup == (LAM f p. Ifup(f)(p))"
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	17
d63ffafce255 * empty log message * oheimb parents: diff changeset	18	translations
10834 a7897aebbffc * empty log message * nipkow parents: 3842 diff changeset	19	"case l of up$x => t1" == "fup$(LAM x. t1)$l"
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	20
d63ffafce255 * empty log message * oheimb parents: diff changeset	21	end
d63ffafce255 * empty log message * oheimb parents: diff changeset	22
d63ffafce255 * empty log message * oheimb parents: diff changeset	23
d63ffafce255 * empty log message * oheimb parents: diff changeset	24

author	nipkow
	Mon, 13 Dec 2004 18:41:49 +0100
changeset 15407	9e85d2b04867
parent 14981	e73f8140af78
permissions	-rw-r--r--