Up to index of Isabelle/HOLCF
theory HOLCF(* Title: HOLCF/HOLCF.thy ID: $Id: HOLCF.thy,v 1.17 2005/09/23 20:21:52 wenzelm Exp $ Author: Franz Regensburger HOLCF -- a semantic extension of HOL by the LCF logic. *) theory HOLCF imports Sprod Ssum Up Lift Discrete One Tr Domain uses "holcf_logic.ML" "cont_consts.ML" "domain/library.ML" "domain/syntax.ML" "domain/axioms.ML" "domain/theorems.ML" "domain/extender.ML" "domain/interface.ML" "adm_tac.ML" begin ML_setup {* simpset_ref() := simpset() addSolver (mk_solver' "adm_tac" (fn ss => adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))); *} end