3 no_document use_thy "Base";

     3 no_document use_thy "Base";

     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 "Parsing";

     9 use_thy "Parsing";

     9 use_thy "Tactical";

    10 use_thy "Tactical";

    10 

    11 

    11 use_thy "Package/Ind_Intro";

    12 use_thy "Package/Ind_Intro";

    12 use_thy "Package/Ind_Prelims";

    13 use_thy "Package/Ind_Prelims";