author | desharna |
Sat, 18 Dec 2021 23:11:49 +0100 | |
changeset 74953 | aade20a03edb |
parent 65378 | 4bb51e6334ed |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/HOLCF.thy |
1479 | 2 |
Author: Franz Regensburger |
65378 | 3 |
Author: Brian Huffman |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
|
16841 | 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 | 8 |
theory HOLCF |
29130 | 9 |
imports |
35473 | 10 |
Main |
11 |
Domain |
|
12 |
Powerdomains |
|
15650 | 13 |
begin |
14 |
||
40497 | 15 |
default_sort "domain" |
25904 | 16 |
|
15650 | 17 |
end |