doc-src/IsarImplementation/Thy/ROOT.ML

--- a/doc-src/IsarImplementation/Thy/ROOT.ML	Wed Mar 04 10:43:39 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ROOT.ML	Wed Mar 04 10:45:52 2009 +0100
@@ -1,11 +1,11 @@
-
-(* $Id$ *)
-
-use_thy "prelim";
-use_thy "logic";
-use_thy "tactic";
-use_thy "proof";
-use_thy "isar";
-use_thy "locale";
-use_thy "integration";
-use_thy "ML";
+use_thys [
+  "Integration",
+  "Isar",
+  "Local_Theory",
+  "Logic",
+  "ML",
+  "Prelim",
+  "Proof",
+  "Syntax",
+  "Tactic"
+];