isabelle: src/HOLCF/Up2.thy@f88a91ff8ac6 (annotated)

2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	1	(* Title: HOLCF/Up2.thy
d63ffafce255 * empty log message * oheimb parents: diff changeset	2	ID: $Id$
d63ffafce255 * empty log message * oheimb parents: diff changeset	3	Author: Franz Regensburger
12030 46d57d0290a2 GPLed; wenzelm parents: 2640 diff changeset	4	License: GPL (GNU GENERAL PUBLIC LICENSE)
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	5
d63ffafce255 * empty log message * oheimb parents: diff changeset	6	Class Instance u::(pcpo)po
d63ffafce255 * empty log message * oheimb parents: diff changeset	7	*)
d63ffafce255 * empty log message * oheimb parents: diff changeset	8
d63ffafce255 * empty log message * oheimb parents: diff changeset	9	Up2 = Up1 +
d63ffafce255 * empty log message * oheimb parents: diff changeset	10
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2278 diff changeset	11	instance u :: (pcpo)po (refl_less_up,antisym_less_up,trans_less_up)
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	12
d63ffafce255 * empty log message * oheimb parents: diff changeset	13	end
d63ffafce255 * empty log message * oheimb parents: diff changeset	14
d63ffafce255 * empty log message * oheimb parents: diff changeset	15
d63ffafce255 * empty log message * oheimb parents: diff changeset	16