isabelle: src/HOLCF/Pcpo.thy@0ef6ea27ab15 (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
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	6	consts
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	7	UU :: "'a::pcpo"
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 628 diff changeset	8
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	9	rules
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	10
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	11	minimal "UU << x"
21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	12	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	13
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	14	inst_void_pcpo "(UU::void) = UU_void"
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	15
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 628 diff changeset	16	(* start 8bit 1 *)
ea0668a1c0ba added 8bit pragmas regensbu parents: 628 diff changeset	17	(* end 8bit 1 *)
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	18	end

author	paulson
	Thu, 21 Mar 1996 13:02:26 +0100
changeset 1601	0ef6ea27ab15
parent 1479	21eb5e156d91
child 2278	d63ffafce255
permissions	-rw-r--r--