doc-src/TutorialI/Ifexpr/ROOT.ML
changeset 9834 109b11c4e77e
parent 8745 13b32661dde4
equal deleted inserted replaced
9833:193dc80eaee9 9834:109b11c4e77e
       
     1 use "../settings.ML";
     1 use_thy "Ifexpr";
     2 use_thy "Ifexpr";