ProgTutorial/ROOT.ML
changeset 329 5dffcab68680
parent 328 c0cae24b9d46
child 348 2f2018927f2a
equal deleted inserted replaced
328:c0cae24b9d46 329:5dffcab68680
     4 no_document use_thy "Package/Simple_Inductive_Package";
     4 no_document use_thy "Package/Simple_Inductive_Package";
     5 
     5 
     6 use_thy "Intro";
     6 use_thy "Intro";
     7 use_thy "FirstSteps";
     7 use_thy "FirstSteps";
     8 use_thy "General";
     8 use_thy "General";
       
     9 
       
    10 no_document use_thy "Helper/Command/Command";
     9 use_thy "Parsing";
    11 use_thy "Parsing";
    10 use_thy "Tactical";
    12 use_thy "Tactical";
    11 
    13 
    12 use_thy "Package/Ind_Intro";
    14 use_thy "Package/Ind_Intro";
    13 use_thy "Package/Ind_Prelims";
    15 use_thy "Package/Ind_Prelims";