# HG changeset patch
# User wenzelm
# Date 1235835333 -3600
# Node ID faf7b2ba1fefd13397254b6480735d332fa91e4c
# Parent  f47c812de07c4890c79ddff6a44b6e739f57709e
simultaneous use_thys;

diff -r f47c812de07c -r faf7b2ba1fef doc-src/IsarRef/Thy/ROOT.ML
--- 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"
+];