--- a/doc-src/TutorialI/Recdef/ROOT.ML Thu Aug 17 21:07:25 2000 +0200 +++ b/doc-src/TutorialI/Recdef/ROOT.ML Fri Aug 18 10:34:08 2000 +0200 @@ -1,2 +1,3 @@ use_thy "termination"; use_thy "Induction"; +(*use_thy "Nested1";*)