isabelle: src/HOL/HOLCF/HOLCF.thy@6ac273f176cd (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41886 diff changeset	1	(* Title: HOL/HOLCF/HOLCF.thy
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	2	Author: Franz Regensburger
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	3
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	4	HOLCF -- a semantic extension of HOL by the LCF logic.
243 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
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	7	theory HOLCF
29130 685c9e05a6ab new theory Dsum: cpo of disjoint sum huffman parents: 28892 diff changeset	8	imports
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	9	Main
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	10	Domain
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	11	Powerdomains
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	12	begin
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	13
40497 d2e876d6da8c rename class 'bifinite' to 'domain' huffman parents: 40431 diff changeset	14	default_sort "domain"
25904 8161f137b0e9 new theory of powerdomains huffman parents: 23152 diff changeset	15
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	16	end

author	blanchet
	Mon, 16 Dec 2013 12:26:18 +0100
changeset 54766	6ac273f176cd
parent 45049	13efaee97111
child 65378	4bb51e6334ed
permissions	-rw-r--r--