author | huffman |
Sun, 19 Dec 2010 05:15:31 -0800 | |
changeset 41286 | 3d7685a4a5ff |
parent 40774 | 0437dbc127b3 |
child 41413 | 64cd30d6b0b8 |
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"]; |