1.1 --- a/src/HOLCF/HOLCF.thy	Thu Jul 14 19:28:22 2005 +0200
     1.2 +++ b/src/HOLCF/HOLCF.thy	Thu Jul 14 19:28:23 2005 +0200
     1.3 @@ -2,11 +2,27 @@
     1.4      ID:         $Id$
     1.5      Author:     Franz Regensburger
     1.6  
     1.7 -Top theory for HOLCF system.
     1.8 +HOLCF -- a semantic extension of HOL by the LCF logic.
     1.9  *)
    1.10  
    1.11  theory HOLCF
    1.12  imports Sprod Ssum Up Lift Discrete One Tr Domain
    1.13 +uses
    1.14 +  "holcf_logic.ML"
    1.15 +  "cont_consts.ML"
    1.16 +  "domain/library.ML"
    1.17 +  "domain/syntax.ML"
    1.18 +  "domain/axioms.ML"
    1.19 +  "domain/theorems.ML"
    1.20 +  "domain/extender.ML"
    1.21 +  "domain/interface.ML"
    1.22 +  "adm_tac.ML"
    1.23 +
    1.24  begin
    1.25  
    1.26 +ML_setup {*
    1.27 +  simpset_ref() := simpset() addSolver
    1.28 +     (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
    1.29 +*}
    1.30 +
    1.31  end