doc-src/TutorialI/Datatype/ROOT.ML
changeset 8745 13b32661dde4
child 8751 9ed0548177fb
equal deleted inserted replaced
8744:22fa8b16c3ae 8745:13b32661dde4
       
     1 use_thy "ABexpr";
       
     2 use_thy "Nested";
       
     3 use_thy "Fundata";