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"; |
5 no_document use_thy "~~/src/HOL/Number_Theory/Primes"; |
6 no_document use_thy "Efficient_Nat"; |
6 no_document use_thy "~~/src/HOL/Library/Efficient_Nat"; |
7 |
7 |
8 use_thy "Intro"; |
8 use_thy "Intro"; |
9 use_thy "First_Steps"; |
9 use_thy "First_Steps"; |
10 use_thy "Essential"; |
10 use_thy "Essential"; |
11 use_thy "Advanced"; |
11 use_thy "Advanced"; |