changeset 328 | c0cae24b9d46 |
parent 327 | ce754ad78bc9 |
child 329 | 5dffcab68680 |
327:ce754ad78bc9 | 328:c0cae24b9d46 |
---|---|
1 set quick_and_dirty; |
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 |
5 |
6 use_thy "Intro"; |
6 use_thy "Intro"; |