equal
deleted
inserted
replaced
1 (*show_question_marks := false;*) |
1 (*show_question_marks := false;*) |
2 |
2 |
3 no_document use_thy "LaTeXsugar"; |
3 no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; |
4 quick_and_dirty := true; |
4 quick_and_dirty := true; |
5 use_thy "Slides" |
5 use_thy "Slides" |