equal
deleted
inserted
replaced
1 set quick_and_dirty; |
1 set quick_and_dirty; |
|
2 |
|
3 no_document use_thy "Base"; |
2 |
4 |
3 use_thy "Intro"; |
5 use_thy "Intro"; |
4 use_thy "FirstSteps"; |
6 use_thy "FirstSteps"; |
5 use_thy "Parsing"; |
7 use_thy "Parsing"; |
|
8 |
|
9 no_document use_thy "Package/Simple_Inductive_Package"; |
|
10 use_thy "Package/Ind_Intro"; |
|
11 use_thy "Package/Ind_Examples"; |
|
12 use_thy "Package/Ind_General_Scheme"; |
|
13 use_thy "Package/Ind_Interface"; |
6 |
14 |
7 use_thy "Appendix"; |
15 use_thy "Appendix"; |
8 use_thy "Recipes/NamedThms"; |
16 use_thy "Recipes/NamedThms"; |
9 use_thy "Recipes/Transformation"; |
17 use_thy "Recipes/Transformation"; |
10 |
18 |