changeset 16841 | 228d663cc9b3 |
parent 16062 | f8110bd9957f |
--- a/src/HOLCF/HOLCF.ML Thu Jul 14 19:28:22 2005 +0200 +++ b/src/HOLCF/HOLCF.ML Thu Jul 14 19:28:23 2005 +0200 @@ -1,16 +1,8 @@ (* Title: HOLCF/HOLCF.ML ID: $Id$ - Author: Franz Regensburger *) structure HOLCF = struct val thy = the_context (); end; - -use "adm_tac.ML"; - -simpset_ref() := simpset() addSolver - (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs)))); - -val HOLCF_ss = simpset();