author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12030 | 46d57d0290a2 |
child 15650 | b37dc98fbbc5 |
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 |
|
3661 | 6 |
use"adm.ML"; |
7 |
||
7570 | 8 |
simpset_ref() := simpset() addSolver |
9 |
(mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs)))); |
|
3661 | 10 |
|
4098 | 11 |
val HOLCF_ss = simpset(); |