equal
deleted
inserted
replaced
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"; |
5 no_document use_thy "~~/src/HOL/Number_Theory/Primes"; |
6 no_document use_thy "Efficient_Nat"; |
6 no_document use_thy "Efficient_Nat"; |
7 |
7 |
8 use_thy "Intro"; |
8 use_thy "Intro"; |
9 use_thy "FirstSteps"; |
9 use_thy "First_Steps"; |
10 use_thy "Essential"; |
10 use_thy "Essential"; |
11 use_thy "Advanced"; |
11 use_thy "Advanced"; |
12 |
12 |
13 no_document use_thy "Helper/Command/Command"; |
13 no_document use_thy "Helper/Command/Command"; |
14 use_thy "Parsing"; |
14 use_thy "Parsing"; |