| changeset 2748 | 6f38e357b337 |
| parent 2485 | 6bab47906dbe |
| 2747:a5da7b6aff8f | 2748:6f38e357b337 |
|---|---|
1 (* show_question_marks := false; *) |
1 (* show_question_marks := false; *) |
2 |
2 |
3 quick_and_dirty := true; |
3 quick_and_dirty := true; |
4 |
4 |
5 |
5 |
6 no_document use_thy "LaTeXsugar"; |
6 no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; |
7 |
7 |
8 use_thy "Slides2" |
8 use_thy "Slides2" |