# HG changeset patch
# User nipkow
# Date 964175408 -7200
# Node ID a1b31d61f8e124e04c742afc9d4ac2262e9f87cd
# Parent  1c9851cdfe9f3d46f7df7fd0f476b05246021e5f
*** empty log message ***

diff -r 1c9851cdfe9f -r a1b31d61f8e1 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Fri Jul 21 10:28:32 2000 +0200
+++ b/src/HOL/HOL.ML	Fri Jul 21 12:30:08 2000 +0200
@@ -1,4 +1,3 @@
-
 structure HOL =
 struct
   val thy = the_context ();