author | nipkow |
Mon, 02 Mar 2009 16:53:55 +0100 | |
changeset 30198 | 922f944f03b2 |
parent 29542 | d20f453eb4a3 |
child 30603 | 71180005f251 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/HOLCF.thy |
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 |
|
15650 | 7 |
theory HOLCF |
29130 | 8 |
imports |
29534 | 9 |
Domain ConvexPD Algebraic Universal Sum_Cpo Main |
16841 | 10 |
uses |
11 |
"holcf_logic.ML" |
|
23152 | 12 |
"Tools/cont_consts.ML" |
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29355
diff
changeset
|
13 |
"Tools/cont_proc.ML" |
23152 | 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" |
|
15650 | 20 |
begin |
21 |
||
25904 | 22 |
defaultsort pcpo |
23 |
||
26339 | 24 |
declaration {* fn _ => |
25 |
Simplifier.map_ss (fn simpset => simpset addSolver |
|
17612 | 26 |
(mk_solver' "adm_tac" (fn ss => |
29355 | 27 |
Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
16841 | 28 |
*} |
29 |
||
15650 | 30 |
end |