author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 16062 | f8110bd9957f |
child 16841 | 228d663cc9b3 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: HOLCF/HOLCF.ML |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
15650 | 6 |
structure HOLCF = |
7 |
struct |
|
8 |
val thy = the_context (); |
|
9 |
end; |
|
10 |
||
16062
f8110bd9957f
cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other
paulson
parents:
15650
diff
changeset
|
11 |
use "adm_tac.ML"; |
3661 | 12 |
|
7570 | 13 |
simpset_ref() := simpset() addSolver |
14 |
(mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs)))); |
|
3661 | 15 |
|
4098 | 16 |
val HOLCF_ss = simpset(); |