author | huffman |
Tue, 16 Dec 2008 09:44:59 -0800 | |
changeset 29130 | 685c9e05a6ab |
parent 28892 | 435f3718ed9d |
child 29138 | 661a8db7e647 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/HOLCF.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
|
16841 | 5 |
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
|
6 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
|
15650 | 8 |
theory HOLCF |
29130 | 9 |
imports |
10 |
Domain ConvexPD Algebraic Universal Dsum Main |
|
16841 | 11 |
uses |
12 |
"holcf_logic.ML" |
|
23152 | 13 |
"Tools/cont_consts.ML" |
14 |
"Tools/domain/domain_library.ML" |
|
15 |
"Tools/domain/domain_syntax.ML" |
|
16 |
"Tools/domain/domain_axioms.ML" |
|
17 |
"Tools/domain/domain_theorems.ML" |
|
18 |
"Tools/domain/domain_extender.ML" |
|
19 |
"Tools/adm_tac.ML" |
|
16841 | 20 |
|
15650 | 21 |
begin |
22 |
||
25904 | 23 |
defaultsort pcpo |
24 |
||
26339 | 25 |
declaration {* fn _ => |
26 |
Simplifier.map_ss (fn simpset => simpset addSolver |
|
17612 | 27 |
(mk_solver' "adm_tac" (fn ss => |
17876 | 28 |
adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
16841 | 29 |
*} |
30 |
||
15650 | 31 |
end |