src/HOL/Hoare/ROOT.ML

--- a/src/HOL/Hoare/ROOT.ML	Tue Feb 23 10:11:12 2010 +0100
+++ b/src/HOL/Hoare/ROOT.ML	Tue Feb 23 10:11:15 2010 +0100
@@ -1,8 +1,2 @@
-(*  Title:      HOL/Hoare/ROOT.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow
-    Copyright   1998-2003 TUM
-*)
 
-use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples",
-  "Pointer_ExamplesAbort", "SchorrWaite", "Separation"];
+use_thy "Hoare";