isabelle: src/HOLCF/Pcpo.thy@51993fea433f (annotated)

243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	1	Pcpo = Porder +
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	2
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3	classes pcpo < po
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	4
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5	arities void :: pcpo
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	7	consts
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	8
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	9	UU :: "'a::pcpo"
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	10
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	11	syntax (symbols)
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	12
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	13	UU :: "'a::pcpo" ("\\<bottom>")
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 628 diff changeset	14
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15	rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	16
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	17	minimal "UU << x"
91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	18	cpo "is_chain S ==> ? x. range(S) <<\| (x::'a::pcpo)"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	19
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	20	inst_void_pcpo "(UU::void) = UU_void"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	21
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	22	end

author	oheimb
	Wed, 18 Dec 1996 15:16:13 +0100
changeset 2445	51993fea433f
parent 2394	91d8abf108be
child 2640	ee4dfce170a0
permissions	-rw-r--r--