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