diff -r 883b38196dba -r a9cb6a51efc3 Paper/ROOT.ML --- a/Paper/ROOT.ML Thu Mar 18 11:36:03 2010 +0100 +++ b/Paper/ROOT.ML Thu Mar 18 11:37:10 2010 +0100 @@ -1,2 +1,3 @@ quick_and_dirty := true; +no_document use_thys ["LaTeXsugar"]; use_thys ["Paper"]; \ No newline at end of file