--- a/src/HOL/main.ML Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/main.ML Fri Jan 02 00:21:59 2009 +0100
@@ -1,7 +1,2 @@
-(* Title: HOL/main.ML
- ID: $Id$
-
-Classical Higher-order Logic -- only "Main".
-*)
-
+(*side-entry for HOL-Main*)
use_thy "Main";