--- 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*)