isabelle: src/HOLCF/Lift2.thy@5ac837d98a85 (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$
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	3	Author: Olaf Mueller, Robert Sandner
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
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	11	default term
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	arities "lift" :: (term)po
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	14
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	15	rules
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	16
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	17	inst_lift_po "((op <<)::['a lift,'a lift]=>bool) = less_lift"
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	18
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	19	end
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	20

author	paulson
	Mon, 10 Feb 1997 12:34:54 +0100
changeset 2602	5ac837d98a85
parent 2357	dd2e5e655fd2
child 2640	ee4dfce170a0
permissions	-rw-r--r--