equal
deleted
inserted
replaced
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 "Slides3" |
6 use_thy "Slides3" |