doc-src/TutorialI/Datatype/ROOT.ML
changeset 9834 109b11c4e77e
parent 9689 751fde5307e4
equal deleted inserted replaced
9833:193dc80eaee9 9834:109b11c4e77e
       
     1 use "../settings.ML";
     1 use_thy "ABexpr";
     2 use_thy "ABexpr";
     2 use_thy "unfoldnested";
     3 use_thy "unfoldnested";
     3 use_thy "Nested";
     4 use_thy "Nested";
     4 use_thy "Fundata";
     5 use_thy "Fundata";