doc-src/TutorialI/Fun/ROOT.ML
changeset 38324 749a3e6eb0f4
parent 25260 71b2a1fefb84
equal deleted inserted replaced
38323:dc2a61b98bab 38324:749a3e6eb0f4
     1 use "../settings";
     1 use "../settings.ML";
     2 use_thy "fun0";
     2 use_thy "fun0";