--- a/doc-src/System/Thy/ROOT.ML Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/System/Thy/ROOT.ML Tue Nov 18 18:25:10 2008 +0100 @@ -7,4 +7,3 @@ use_thy "Basics"; use_thy "Presentation"; use_thy "Misc"; -use_thy "Symbols";