# HG changeset patch
# User wenzelm
# Date 935687066 -7200
# Node ID 6407a09ac58f2b6243f11d1cac333ef5a4db9032
# Parent  2d2110cda81e4064b6abf264e7bb35044663c3fc
tuned;

diff -r 2d2110cda81e -r 6407a09ac58f src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Aug 26 19:04:19 1999 +0200
+++ b/src/HOL/ROOT.ML	Thu Aug 26 19:04:26 1999 +0200
@@ -15,6 +15,7 @@
 (*old-style theory syntax*)
 use "~~/src/Pure/section_utils.ML";
 use "thy_syntax.ML";
+
 use "hologic.ML";
 
 use "~~/src/Provers/simplifier.ML";
@@ -34,7 +35,6 @@
 
 use_thy "subset";
 use "Tools/typedef_package.ML";
-
 use_thy "Inductive";
 use_thy "NatDef";