diff -r a5da7b6aff8f -r 6f38e357b337 Slides/ROOT3.ML --- a/Slides/ROOT3.ML Wed Mar 16 21:14:43 2011 +0100 +++ b/Slides/ROOT3.ML Tue Mar 29 23:52:14 2011 +0200 @@ -1,6 +1,6 @@ -show_question_marks := false; +(*show_question_marks := false;*) quick_and_dirty := true; -no_document use_thy "LaTeXsugar"; +no_document use_thy "~~/src/HOL/Library/LaTeXsugar"; use_thy "Slides3" \ No newline at end of file