doc-src/TutorialI/CodeGen/ROOT.ML
changeset 9834 109b11c4e77e
parent 8744 22fa8b16c3ae
equal deleted inserted replaced
9833:193dc80eaee9 9834:109b11c4e77e
       
     1 use "../settings.ML";
     1 use_thy "CodeGen";
     2 use_thy "CodeGen";