--- a/doc-src/TutorialI/Misc/ROOT.ML Mon Mar 12 18:23:11 2001 +0100
+++ b/doc-src/TutorialI/Misc/ROOT.ML Tue Mar 13 18:35:48 2001 +0100
@@ -8,6 +8,7 @@
use_thy "Option2";
use_thy "types";
use_thy "prime_def";
+use_thy "Translations";
use_thy "simp";
use_thy "Itrev";
use_thy "AdvancedInd";