| author | huffman |
| Tue, 16 Dec 2008 21:31:55 -0800 | |
| changeset 29138 | 661a8db7e647 |
| parent 29130 | 685c9e05a6ab |
| child 29354 | 642cac18e155 |
| permissions | -rw-r--r-- |
| clasohm@1479 | 1 |
(* Title: HOLCF/HOLCF.thy |
| clasohm@1479 | 2 |
Author: Franz Regensburger |
| nipkow@243 | 3 |
|
| wenzelm@16841 | 4 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
| nipkow@243 | 5 |
*) |
| nipkow@243 | 6 |
|
| huffman@15650 | 7 |
theory HOLCF |
| huffman@29130 | 8 |
imports |
| huffman@29130 | 9 |
Domain ConvexPD Algebraic Universal Dsum Main |
| wenzelm@16841 | 10 |
uses |
| wenzelm@16841 | 11 |
"holcf_logic.ML" |
| wenzelm@23152 | 12 |
"Tools/cont_consts.ML" |
| wenzelm@23152 | 13 |
"Tools/domain/domain_library.ML" |
| wenzelm@23152 | 14 |
"Tools/domain/domain_syntax.ML" |
| wenzelm@23152 | 15 |
"Tools/domain/domain_axioms.ML" |
| wenzelm@23152 | 16 |
"Tools/domain/domain_theorems.ML" |
| wenzelm@23152 | 17 |
"Tools/domain/domain_extender.ML" |
| wenzelm@23152 | 18 |
"Tools/adm_tac.ML" |
| wenzelm@16841 | 19 |
|
| huffman@15650 | 20 |
begin |
| huffman@15650 | 21 |
|
| huffman@25904 | 22 |
defaultsort pcpo |
| huffman@25904 | 23 |
|
| wenzelm@26339 | 24 |
declaration {* fn _ =>
|
| wenzelm@26339 | 25 |
Simplifier.map_ss (fn simpset => simpset addSolver |
| wenzelm@17612 | 26 |
(mk_solver' "adm_tac" (fn ss => |
| wenzelm@17876 | 27 |
adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); |
| wenzelm@16841 | 28 |
*} |
| wenzelm@16841 | 29 |
|
| huffman@15650 | 30 |
end |