--- a/src/HOL/plain.ML Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/plain.ML Fri Jan 02 00:21:59 2009 +0100
@@ -1,6 +1,2 @@
-(* Title: HOL/plain.ML
-
-Classical Higher-order Logic -- plain Tool bootstrap.
-*)
-
+(*side-entry for HOL-Plain*)
use_thy "Plain";