# HG changeset patch
# User wenzelm
# Date 1162990115 -3600
# Node ID e0e555b67fe514dfaddf7ccfaecc46361ae26b41
# Parent  23e6eb4d09758db9030acf75311f3cc7a16fd693
added structure Main (from Main.ML);

diff -r 23e6eb4d0975 -r e0e555b67fe5 src/HOL/ROOT.ML
--- 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*)