isabelle: src/HOLCF/Lift.thy@a5839ecee7b8 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	1	(* Title: HOLCF/Lift.thy
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	2	ID: $Id$
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	3	Author: Oscar Slotosch
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	4	Copyright 1997 Technische Universitaet Muenchen
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	5	*)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	6
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	7	Lift = Lift3 +
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	8
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	9	instance lift :: (term)flat (ax_flat_lift)
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	10
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	11	default pcpo
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	12
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	13	end
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	14
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	15
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: diff changeset	16

author	wenzelm
	Wed, 15 Oct 1997 15:12:59 +0200
changeset 3872	a5839ecee7b8
parent 2640	ee4dfce170a0
child 12026	0b1d80ada4ab
permissions	-rw-r--r--