--- a/doc-src/TutorialI/Recdef/ROOT.ML Mon Sep 04 21:20:14 2000 +0200 +++ b/doc-src/TutorialI/Recdef/ROOT.ML Tue Sep 05 09:03:17 2000 +0200 @@ -1,3 +1,4 @@ +use "../settings"; use_thy "termination"; use_thy "Induction"; use_thy "Nested1";