src/ZF/Constructible/ROOT.ML

--- a/src/ZF/Constructible/ROOT.ML	Mon Jun 24 11:59:14 2002 +0200
+++ b/src/ZF/Constructible/ROOT.ML	Mon Jun 24 11:59:21 2002 +0200
@@ -1,4 +1,11 @@
+(*  Title:      ZF/Constructible/ROOT.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2002  University of Cambridge
+
+Inner Models and Absoluteness
+*)
+
 use_thy "Reflection";
 use_thy "WFrec";
-use_thy "WF_extras";
 use_thy "L_axioms";