diff -r 3d5aad11bc24 -r 228d663cc9b3 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Thu Jul 14 19:28:22 2005 +0200
+++ b/src/HOLCF/HOLCF.thy	Thu Jul 14 19:28:23 2005 +0200
@@ -2,11 +2,27 @@
     ID:         $Id$
     Author:     Franz Regensburger
 
-Top theory for HOLCF system.
+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 thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
+*}
+
 end