src/HOL/Import/HOL/ROOT.ML
changeset 14620 1be590fd2422
parent 14516 a183dec876ab
child 14652 5ddbdbadba06
--- a/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/HOL/ROOT.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 with_path ".." use_thy "HOL4Compat";
 with_path ".." use_thy "HOL4Syntax";
 setmp quick_and_dirty true use_thy "HOL4Prob";