isabelle: src/HOLCF/Pcpo.thy@909079af97b7 (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"
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
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 628 diff changeset	11	minimal "UU << x"
ea0668a1c0ba added 8bit pragmas regensbu parents: 628 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
442 13ac1fd0a14d added parentheses made necessary by change of constrain's precedence clasohm parents: 243 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	clasohm
	Fri, 13 Oct 1995 11:48:40 +0100
changeset 1280	909079af97b7
parent 1274	ea0668a1c0ba
child 1479	21eb5e156d91
permissions	-rw-r--r--