# HG changeset patch
# User paulson
# Date 842517311 -7200
# Node ID 38aafcab689092d022f88eb271ac60529ad889e6
# Parent  432db3edccdcd8a8522790fd2a5098fdf8d2e753
Now hologic.ML is loaded in HOL.ML

diff -r 432db3edccdc -r 38aafcab6890 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Sep 12 10:34:21 1996 +0200
+++ b/src/HOL/ROOT.ML	Thu Sep 12 10:35:11 1996 +0200
@@ -22,10 +22,8 @@
 
 
 use_thy "HOL";
-
 use_thy "Ord";
 use_thy "subset";
-use     "hologic.ML";
 use     "typedef.ML";
 use_thy "Sum";
 use_thy "Gfp";