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";