(* Title: HOLCF/HOLCF.thy
Author: Franz Regensburger
HOLCF -- a semantic extension of HOL by the LCF logic.
*)
theory HOLCF
imports
Domain ConvexPD Algebraic Universal Sum_Cpo Main
uses
"holcf_logic.ML"
"Tools/cont_consts.ML"
"Tools/cont_proc.ML"
"Tools/domain/domain_library.ML"
"Tools/domain/domain_syntax.ML"
"Tools/domain/domain_axioms.ML"
"Tools/domain/domain_theorems.ML"
"Tools/domain/domain_extender.ML"
"Tools/adm_tac.ML"
begin
defaultsort pcpo
declaration {* fn _ =>
Simplifier.map_ss (fn simpset => simpset addSolver
(mk_solver' "adm_tac" (fn ss =>
Adm.adm_tac (Simplifier.the_context ss)
(cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
*}
end