--- a/doc-src/TutorialI/Recdef/ROOT.ML Wed Oct 11 09:09:06 2000 +0200 +++ b/doc-src/TutorialI/Recdef/ROOT.ML Wed Oct 11 10:44:42 2000 +0200 @@ -3,4 +3,3 @@ use_thy "Induction"; use_thy "Nested1"; use_thy "Nested2"; -use_thy "WFrec";