author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
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 |