diff -r 499637e8f2c6 -r 0376cccd9118 doc-src/TutorialI/Recdef/ROOT.ML --- 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";