src/HOL/HOLCF/HOLCF.thy
author wenzelm
Tue, 04 Apr 2017 21:44:44 +0200
changeset 65378 4bb51e6334ed
parent 45049 13efaee97111
permissions -rw-r--r--
tuned header;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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