isabelle: src/HOLCF/Lift1.thy@412c62dd43de (annotated)

2357 dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	1	(* Title: HOLCF/Lift1.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	Lifting types of class term to flat pcpo's
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	7	*)
dd2e5e655fd2 Headers added sandnerr parents: 2356 diff changeset	8
3327 9b8e638f8602 Eliminated ccc1. Moved ID,oo into Cfun. slotosch parents: 3323 diff changeset	9	Lift1 = Cprod3 +
2356 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
2394 91d8abf108be adaptions for symbol font oheimb parents: 2357 diff changeset	13	datatype 'a lift = Undef \| Def 'a
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	14
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3033 diff changeset	15	instance lift :: (term)sq_ord
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	16	defs
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	17
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3033 diff changeset	18	less_lift_def "x << y == (x=y \| x=Undef)"
2356 125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	19
125260ef480c Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy sandnerr parents: diff changeset	20	end

author	wenzelm
	Tue, 05 Aug 1997 16:43:54 +0200
changeset 3591	412c62dd43de
parent 3327	9b8e638f8602
child 5192	704dd3a6d47d
permissions	-rw-r--r--