isabelle: src/HOLCF/Pcpo.thy@fbd14a05fb88 (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	oheimb
	Mon, 02 Dec 1996 12:37:15 +0100
changeset 2291	fbd14a05fb88
parent 2278	d63ffafce255
child 2394	91d8abf108be
permissions	-rw-r--r--