# HG changeset patch
# User haftmann
# Date 1201269238 -3600
# Node ID 080f89d89990f0a6f9441b0821743bb6b42cc8b3
# Parent  07e08dad8a7733f7252970e64f10c32f85aabdca
consistent interacitve bootstrap of HOL-Main

diff -r 07e08dad8a77 -r 080f89d89990 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Jan 25 14:53:56 2008 +0100
+++ b/src/HOL/Main.thy	Fri Jan 25 14:53:58 2008 +0100
@@ -15,4 +15,6 @@
 
 ML {* val HOL_proofs = ! Proofterm.proofs *}
 
+ML {* path_add "~~/src/HOL/Library" *}
+
 end
diff -r 07e08dad8a77 -r 080f89d89990 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Jan 25 14:53:56 2008 +0100
+++ b/src/HOL/ROOT.ML	Fri Jan 25 14:53:58 2008 +0100
@@ -5,5 +5,3 @@
 *)
 
 use_thy "Main";
-
-path_add "~~/src/HOL/Library";