changeset 203 | 5d724fe0e096 |
parent 24 | f72c82bf59e5 |
--- a/Slides/ROOT.ML Fri Aug 19 20:39:07 2011 +0000 +++ b/Slides/ROOT.ML Mon Aug 22 12:49:27 2011 +0000 @@ -1,5 +1,5 @@ (*show_question_marks := false;*) -no_document use_thy "LaTeXsugar"; +no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; quick_and_dirty := true; use_thy "Slides" \ No newline at end of file