isabelle: src/HOLCF/Lift2.thy@a9391550eea1 (annotated)

2357 dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	1	(* Title: HOLCF/Lift2.thy
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	2	ID: $Id$
3033 50e14d6d894f only in comments mueller parents: 2640 diff changeset	3	Author: Olaf Mueller
2357 dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	4	Copyright 1996 Technische Universitaet Muenchen
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	5
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	6	Class Instance lift::(term)po
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	7	*)
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	8
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	9	Lift2 = Lift1 +
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	10
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2357 diff changeset	11	instance "lift" :: (term)po (refl_less_lift,antisym_less_lift,trans_less_lift)
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	12
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	13	end
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	14
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2357 diff changeset	15

author	nipkow
	Tue, 21 Sep 1999 19:11:07 +0200
changeset 7570	a9391550eea1
parent 3033	50e14d6d894f
permissions	-rw-r--r--