1.1 --- a/doc-src/IsarRef/Thy/ROOT.ML	Sat Feb 28 16:31:10 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML	Sat Feb 28 16:35:33 2009 +0100
     1.3 @@ -2,17 +2,19 @@
     1.4  set ThyOutput.source;
     1.5  use "../../antiquote_setup.ML";
     1.6  
     1.7 -use_thy "Introduction";
     1.8 -use_thy "Framework";
     1.9 -use_thy "First_Order_Logic";
    1.10 -use_thy "Outer_Syntax";
    1.11 -use_thy "Document_Preparation";
    1.12 -use_thy "Spec";
    1.13 -use_thy "Proof";
    1.14 -use_thy "Inner_Syntax";
    1.15 -use_thy "Misc";
    1.16 -use_thy "Generic";
    1.17 -use_thy "HOL_Specific";
    1.18 -use_thy "Quick_Reference";
    1.19 -use_thy "Symbols";
    1.20 -use_thy "ML_Tactic";
    1.21 +use_thys [
    1.22 +  "Introduction",
    1.23 +  "Framework",
    1.24 +  "First_Order_Logic",
    1.25 +  "Outer_Syntax",
    1.26 +  "Document_Preparation",
    1.27 +  "Spec",
    1.28 +  "Proof",
    1.29 +  "Inner_Syntax",
    1.30 +  "Misc",
    1.31 +  "Generic",
    1.32 +  "HOL_Specific",
    1.33 +  "Quick_Reference",
    1.34 +  "Symbols",
    1.35 +  "ML_Tactic"
    1.36 +];