1 (* Title: HOLCF/HOLCF.thy
2 Author: Franz Regensburger
4 HOLCF -- a semantic extension of HOL by the LCF logic.
9 Domain ConvexPD Algebraic Universal Dsum Main
12 "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"
25 declaration {* fn _ =>
26 Simplifier.map_ss (fn simpset => simpset addSolver
27 (mk_solver' "adm_tac" (fn ss =>
28 Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));