src/HOL/HOLCF/HOLCF.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45049 13efaee97111
child 65378 4bb51e6334ed
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
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