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