--- a/doc-src/TutorialI/Misc/ROOT.ML Tue Aug 01 18:26:34 2000 +0200 +++ b/doc-src/TutorialI/Misc/ROOT.ML Wed Aug 02 11:30:38 2000 +0200 @@ -1,4 +1,5 @@ use_thy "Tree"; +use_thy "Tree2"; use_thy "cases"; use_thy "fakenat"; use_thy "natsum";