equal
deleted
inserted
replaced
1 show_question_marks := false; |
1 (* show_question_marks := false; *) |
|
2 |
2 quick_and_dirty := true; |
3 quick_and_dirty := true; |
|
4 |
3 |
5 |
4 no_document use_thy "LaTeXsugar"; |
6 no_document use_thy "LaTeXsugar"; |
5 |
7 |
6 use_thy "Slides2" |
8 use_thy "Slides2" |