author | huffman |
Wed, 10 Nov 2010 18:37:11 -0800 | |
changeset 40505 | 702708d26c9b |
parent 39982 | 5681f840688b |
permissions | -rw-r--r-- |
3623 | 1 |
(* Title: HOLCF/ROOT.ML |
1461 | 2 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
|
16841 | 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 |
|
39982 | 7 |
no_document use_thys ["Nat_Bijection", "Countable"]; |
29921 | 8 |
|
40505 | 9 |
use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"]; |