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