isabelle: src/HOL/HOLCF/HOLCF.thy@7ab0fb5d9919 (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
65378 4bb51e6334ed tuned header; wenzelm parents: 45049 diff changeset	3	Author: Brian Huffman
243 c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	4
16841 228d663cc9b3 use all files in HOLCF.thy; wenzelm parents: 16054 diff changeset	5	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	6	*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF nipkow parents: diff changeset	7
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	8	theory HOLCF
29130 685c9e05a6ab new theory Dsum: cpo of disjoint sum huffman parents: 28892 diff changeset	9	imports
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	10	Main
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	11	Domain
c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 33588 diff changeset	12	Powerdomains
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	13	begin
b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	14
40497 d2e876d6da8c rename class 'bifinite' to 'domain' huffman parents: 40431 diff changeset	15	default_sort "domain"
25904 8161f137b0e9 new theory of powerdomains huffman parents: 23152 diff changeset	16
15650 b37dc98fbbc5 converted to new-style theory huffman parents: 15576 diff changeset	17	end

author	wenzelm
	Thu, 24 Apr 2025 23:29:57 +0200
changeset 82584	7ab0fb5d9919
parent 65378	4bb51e6334ed
permissions	-rw-r--r--