--- a/src/HOL/Library/ROOT.ML Sun Feb 04 19:43:15 2001 +0100 +++ b/src/HOL/Library/ROOT.ML Sun Feb 04 19:43:32 2001 +0100 @@ -1,1 +1,2 @@ + use_thy "Library";