equal
deleted
inserted
replaced
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 "General"; |
8 use_thy "Essential"; |
|
9 use_thy "Advanced"; |
9 |
10 |
10 no_document use_thy "Helper/Command/Command"; |
11 no_document use_thy "Helper/Command/Command"; |
11 use_thy "Parsing"; |
12 use_thy "Parsing"; |
12 use_thy "Tactical"; |
13 use_thy "Tactical"; |
13 |
14 |