author | wenzelm |
Sat, 14 Jan 2012 12:36:43 +0100 | |
changeset 46204 | df1369a42393 |
parent 42151 | 4da4fc77664b |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/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 |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40774
diff
changeset
|
7 |
no_document use_thys ["~~/src/HOL/Library/Nat_Bijection", "~~/src/HOL/Library/Countable"]; |
29921 | 8 |
|
40505 | 9 |
use_thys ["Plain_HOLCF", "Fixrec", "HOLCF"]; |