# HG changeset patch
# User wenzelm
# Date 1121362103 -7200
# Node ID 228d663cc9b350e05063542c433e833c2ef3eb15
# Parent  3d5aad11bc247f38e2541fe8095444ca8aa3c3f9
use all files in HOLCF.thy;

diff -r 3d5aad11bc24 -r 228d663cc9b3 src/HOLCF/HOLCF.ML
--- 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();
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
diff -r 3d5aad11bc24 -r 228d663cc9b3 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Thu Jul 14 19:28:22 2005 +0200
+++ b/src/HOLCF/ROOT.ML	Thu Jul 14 19:28:23 2005 +0200
@@ -2,23 +2,10 @@
     ID:         $Id$
     Author:     Franz Regensburger
 
-Conservative (semantic) extension of HOL by the LCF logic.
+HOLCF -- a semantic extension of HOL by the LCF logic.
 *)
 
 val banner = "HOLCF";
 writeln banner;
 
 use_thy "HOLCF";
-
-use "holcf_logic.ML";
-use "cont_consts.ML";
-
-(* domain package *)
-use "domain/library.ML";
-use "domain/syntax.ML";
-use "domain/axioms.ML";
-use "domain/theorems.ML";
-use "domain/extender.ML";
-use "domain/interface.ML";
-
-path_add "~~/src/HOLCF/ex";