1 quick_and_dirty := true;

     2 

     3 no_document use_thy "Base";

     4 no_document use_thy "Package/Simple_Inductive_Package";

     5 no_document use_thy "~~/src/HOL/Number_Theory/Primes"; 

     6 no_document use_thy "~~/src/HOL/Library/Efficient_Nat";

     7 

     8 use_thy "Intro";

     9 use_thy "First_Steps";

    10 use_thy "Essential";

    11 use_thy "Advanced";

    12 

    13 no_document use_thy "Helper/Command/Command";

    14 use_thy "Parsing";

    15 use_thy "Tactical";

    16 

    17 use_thy "Package/Ind_Intro";

    18 use_thy "Package/Ind_Prelims";

    19 use_thy "Package/Ind_Interface";

    20 use_thy "Package/Ind_General_Scheme";

    21 use_thy "Package/Ind_Code";

    22 use_thy "Package/Ind_Extensions";

    23 

    24 use_thy "Appendix";

    25 use_thy "Recipes/Antiquotes";

    26 use_thy "Recipes/TimeLimit";

    27 use_thy "Recipes/Timing";

    28 use_thy "Recipes/CallML";

    29 use_thy "Recipes/ExternalSolver";

    30 use_thy "Recipes/Oracle";

    31 use_thy "Recipes/Sat";

    32 use_thy "Recipes/USTypes";

    33 

    34 use_thy "Solutions";

    35 (*use_thy "Readme";*)

    36