--- a/src/HOL/Import/ROOT.ML Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/ROOT.ML Sat Apr 17 23:53:35 2004 +0200
@@ -1,2 +1,7 @@
+(* Title: HOL/Import/ROOT.ML
+ ID: $Id$
+ Author: Sebastian Skalberg (TU Muenchen)
+*)
+
use_thy "HOL4Compat";
use_thy "HOL4Syntax";