isabelle: src/HOLCF/One.thy@804ecdc08cf2 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2275 diff changeset	1	(* Title: HOLCF/One.thy
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2	ID: $Id$
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2275 diff changeset	3	Author: Oscar Slotosch
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2275 diff changeset	6	One = Lift +
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
3717 e28553315355 eliminated rules; wenzelm parents: 2640 diff changeset	8	types one = unit lift
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9
3717 e28553315355 eliminated rules; wenzelm parents: 2640 diff changeset	10	constdefs
e28553315355 eliminated rules; wenzelm parents: 2640 diff changeset	11	ONE :: "one"
e28553315355 eliminated rules; wenzelm parents: 2640 diff changeset	12	"ONE == Def ()"
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2275 diff changeset	13
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2275 diff changeset	14	translations
3717 e28553315355 eliminated rules; wenzelm parents: 2640 diff changeset	15	"one" <= (type) "unit lift"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	17	end

author	paulson
	Mon, 04 Oct 2004 15:25:28 +0200
changeset 15227	804ecdc08cf2
parent 14981	e73f8140af78
child 15576	efb95d0d01f7
permissions	-rw-r--r--