diff -r 68d247b7b14b -r ff6eb32b30a1 src/HOL/Hoare/ROOT.ML
--- a/src/HOL/Hoare/ROOT.ML	Wed May 14 11:15:18 2003 +0200
+++ b/src/HOL/Hoare/ROOT.ML	Wed May 14 14:20:55 2003 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/IMP/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1998 TUM
+    Copyright   1998-2003 TUM
 *)
 
 time_use_thy "Examples";
@@ -10,3 +10,4 @@
 time_use_thy "Pointer_Examples";
 time_use_thy "Pointer_ExamplesAbort";
 time_use_thy "SchorrWaite";
+time_use_thy "Separation";