--- a/doc-src/LaTeXsugar/Sugar/ROOT.ML Thu Feb 03 03:56:11 2005 +0100 +++ b/doc-src/LaTeXsugar/Sugar/ROOT.ML Thu Feb 03 04:09:52 2005 +0100 @@ -1,2 +1,4 @@ +no_document use_thy "LaTeXsugar"; +no_document use_thy "OptionalSugar"; use_thy "Sugar";