--- a/src/HOLCF/HOLCF.ML Fri Apr 01 23:44:41 2005 +0200
+++ b/src/HOLCF/HOLCF.ML Sat Apr 02 00:12:38 2005 +0200
@@ -3,6 +3,11 @@
Author: Franz Regensburger
*)
+structure HOLCF =
+struct
+ val thy = the_context ();
+end;
+
use"adm.ML";
simpset_ref() := simpset() addSolver
--- a/src/HOLCF/HOLCF.thy Fri Apr 01 23:44:41 2005 +0200
+++ b/src/HOLCF/HOLCF.thy Sat Apr 02 00:12:38 2005 +0200
@@ -5,4 +5,8 @@
Top theory for HOLCF system.
*)
-HOLCF = Sprod + Ssum + Up + Lift + Discrete + One + Tr
+theory HOLCF
+imports Sprod Ssum Up Lift Discrete One Tr
+begin
+
+end