--- a/doc-src/IsarRef/Thy/ROOT.ML Sat Feb 28 16:31:10 2009 +0100
+++ b/doc-src/IsarRef/Thy/ROOT.ML Sat Feb 28 16:35:33 2009 +0100
@@ -2,17 +2,19 @@
set ThyOutput.source;
use "../../antiquote_setup.ML";
-use_thy "Introduction";
-use_thy "Framework";
-use_thy "First_Order_Logic";
-use_thy "Outer_Syntax";
-use_thy "Document_Preparation";
-use_thy "Spec";
-use_thy "Proof";
-use_thy "Inner_Syntax";
-use_thy "Misc";
-use_thy "Generic";
-use_thy "HOL_Specific";
-use_thy "Quick_Reference";
-use_thy "Symbols";
-use_thy "ML_Tactic";
+use_thys [
+ "Introduction",
+ "Framework",
+ "First_Order_Logic",
+ "Outer_Syntax",
+ "Document_Preparation",
+ "Spec",
+ "Proof",
+ "Inner_Syntax",
+ "Misc",
+ "Generic",
+ "HOL_Specific",
+ "Quick_Reference",
+ "Symbols",
+ "ML_Tactic"
+];