bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
(* Title: HOLCF/HOLCF.ML
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
use"adm.ML";
simpset_ref() := simpset() addSolver
(mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
val HOLCF_ss = simpset();