isabelle: src/HOLCF/Up2.thy@59bd96046ad6 (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
d63ffafce255 * empty log message * oheimb parents: diff changeset	4	Copyright 1993 Technische Universitaet Muenchen
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
d63ffafce255 * empty log message * oheimb parents: diff changeset	10	Up2 = Up1 +
d63ffafce255 * empty log message * oheimb parents: diff changeset	11
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2278 diff changeset	12	instance u :: (pcpo)po (refl_less_up,antisym_less_up,trans_less_up)
2278 d63ffafce255 * empty log message * oheimb parents: diff changeset	13
d63ffafce255 * empty log message * oheimb parents: diff changeset	14	end
d63ffafce255 * empty log message * oheimb parents: diff changeset	15
d63ffafce255 * empty log message * oheimb parents: diff changeset	16
d63ffafce255 * empty log message * oheimb parents: diff changeset	17

author	wenzelm
	Fri, 07 Mar 1997 11:48:46 +0100
changeset 2754	59bd96046ad6
parent 2640	ee4dfce170a0
child 12030	46d57d0290a2
permissions	-rw-r--r--