isabelle: src/HOLCF/Pcpo.thy@a744f9749885 (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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4	arities void :: pcpo
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	6	consts
625 119391dd1d59 New version nipkow parents: 442 diff changeset	7	UU :: "'a::pcpo"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	8	rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9
625 119391dd1d59 New version nipkow parents: 442 diff changeset	10	minimal "UU << x"
628 bb3f87f9cafe corrected problems with changed binding power of ::. nipkow parents: 625 diff changeset	11	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	12
442 13ac1fd0a14d added parentheses made necessary by change of constrain's precedence clasohm parents: 243 diff changeset	13	inst_void_pcpo "(UU::void) = UU_void"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	14
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15	end

author	lcp
	Thu, 12 Jan 1995 03:00:58 +0100
changeset 850	a744f9749885
parent 628	bb3f87f9cafe
child 1274	ea0668a1c0ba
permissions	-rw-r--r--