--- a/src/HOL/ROOT.ML Wed Nov 08 13:48:34 2006 +0100
+++ b/src/HOL/ROOT.ML Wed Nov 08 13:48:35 2006 +0100
@@ -37,6 +37,11 @@
with_path "Integ" use_thy "Main";
+structure Main =
+struct
+ val thy = theory "Main"
+end;
+
path_add "~~/src/HOL/Library";
Goal "True"; (*leave subgoal package empty*)