--- a/src/HOL/Hoare/ROOT.ML Tue Jul 31 22:21:18 2007 +0200
+++ b/src/HOL/Hoare/ROOT.ML Tue Jul 31 22:21:20 2007 +0200
@@ -4,10 +4,5 @@
Copyright 1998-2003 TUM
*)
-time_use_thy "Examples";
-time_use_thy "ExamplesAbort";
-time_use_thy "Pointers0";
-time_use_thy "Pointer_Examples";
-time_use_thy "Pointer_ExamplesAbort";
-time_use_thy "SchorrWaite";
-time_use_thy "Separation";
+use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples",
+ "Pointer_ExamplesAbort", "SchorrWaite", "Separation"];