doc-src/TutorialI/Misc/ROOT.ML
changeset 13305 f88d0c363582
parent 12582 b85acd66f715
equal deleted inserted replaced
13304:43ef6c6dd906 13305:f88d0c363582
     1 use "../settings.ML";
     1 use "../settings.ML";
     2 use_thy "Tree";
     2 use_thy "Tree";
     3 use_thy "Tree2";
     3 use_thy "Tree2";
       
     4 use_thy "Plus";
     4 use_thy "case_exprs";
     5 use_thy "case_exprs";
     5 use_thy "fakenat";
     6 use_thy "fakenat";
     6 use_thy "natsum";
     7 use_thy "natsum";
     7 use_thy "pairs";
     8 use_thy "pairs";
     8 use_thy "Option2";
     9 use_thy "Option2";