equal
deleted
inserted
replaced
1 (* Title: HOLCF/HOLCF.thy |
1 (* Title: HOLCF/HOLCF.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 |
4 |
5 Top theory for HOLCF system. |
5 HOLCF -- a semantic extension of HOL by the LCF logic. |
6 *) |
6 *) |
7 |
7 |
8 theory HOLCF |
8 theory HOLCF |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain |
|
10 uses |
|
11 "holcf_logic.ML" |
|
12 "cont_consts.ML" |
|
13 "domain/library.ML" |
|
14 "domain/syntax.ML" |
|
15 "domain/axioms.ML" |
|
16 "domain/theorems.ML" |
|
17 "domain/extender.ML" |
|
18 "domain/interface.ML" |
|
19 "adm_tac.ML" |
|
20 |
10 begin |
21 begin |
11 |
22 |
|
23 ML_setup {* |
|
24 simpset_ref() := simpset() addSolver |
|
25 (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs)))); |
|
26 *} |
|
27 |
12 end |
28 end |