doc-src/IsarRef/Thy/ROOT.ML
changeset 30130 e23770bc97c8
parent 29730 924c1fd5f303
child 30167 faf7b2ba1fef
equal deleted inserted replaced
30129:419116f1157a 30130:e23770bc97c8
     1 
     1 set quick_and_dirty;
     2 (* $Id$ *)
       
     3 
       
     4 set ThyOutput.source;
     2 set ThyOutput.source;
     5 use "../../antiquote_setup.ML";
     3 use "../../antiquote_setup.ML";
     6 
     4 
     7 use_thy "Introduction";
     5 use_thy "Introduction";
       
     6 use_thy "Framework";
       
     7 use_thy "First_Order_Logic";
     8 use_thy "Outer_Syntax";
     8 use_thy "Outer_Syntax";
     9 use_thy "Document_Preparation";
     9 use_thy "Document_Preparation";
    10 use_thy "Spec";
    10 use_thy "Spec";
    11 use_thy "Proof";
    11 use_thy "Proof";
    12 use_thy "Inner_Syntax";
    12 use_thy "Inner_Syntax";