doc-src/TutorialI/CodeGen/ROOT.ML
changeset 48519 5deda0549f97
parent 48518 0c86acc069ad
child 48520 6d4ea2efa64b
equal deleted inserted replaced
48518:0c86acc069ad 48519:5deda0549f97
     1 use "../settings.ML";
       
     2 use_thy "CodeGen";