equal
deleted
inserted
replaced
1 quick_and_dirty := true; |
1 quick_and_dirty := true; |
2 |
2 |
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 no_document use_thy "~~/src/HOL/Number_Theory/Primes"; |
|
6 no_document use_thy "Efficient_Nat"; |
5 |
7 |
6 use_thy "Intro"; |
8 use_thy "Intro"; |
7 use_thy "FirstSteps"; |
9 use_thy "FirstSteps"; |
8 use_thy "Essential"; |
10 use_thy "Essential"; |
9 use_thy "Advanced"; |
11 use_thy "Advanced"; |
21 |
23 |
22 use_thy "Appendix"; |
24 use_thy "Appendix"; |
23 use_thy "Recipes/Antiquotes"; |
25 use_thy "Recipes/Antiquotes"; |
24 use_thy "Recipes/TimeLimit"; |
26 use_thy "Recipes/TimeLimit"; |
25 use_thy "Recipes/Timing"; |
27 use_thy "Recipes/Timing"; |
|
28 use_thy "Recipes/CallML"; |
26 use_thy "Recipes/ExternalSolver"; |
29 use_thy "Recipes/ExternalSolver"; |
27 use_thy "Recipes/Oracle"; |
30 use_thy "Recipes/Oracle"; |
28 use_thy "Recipes/Sat"; |
31 use_thy "Recipes/Sat"; |
29 use_thy "Recipes/USTypes"; |
32 use_thy "Recipes/USTypes"; |
30 |
33 |