doc-src/TutorialI/Misc/ROOT.ML
changeset 11203 881222d48777
parent 10978 5eebea8f359f
child 12582 b85acd66f715
     1.1 --- a/doc-src/TutorialI/Misc/ROOT.ML	Mon Mar 12 18:23:11 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Tue Mar 13 18:35:48 2001 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  use_thy "Option2";
     1.5  use_thy "types";
     1.6  use_thy "prime_def";
     1.7 +use_thy "Translations";
     1.8  use_thy "simp";
     1.9  use_thy "Itrev";
    1.10  use_thy "AdvancedInd";