doc-src/TutorialI/Misc/ROOT.ML
changeset 10978 5eebea8f359f
parent 10543 8e4307d1207a
child 11203 881222d48777
equal deleted inserted replaced
10977:4b47d8aaf5af 10978:5eebea8f359f
     9 use_thy "types";
     9 use_thy "types";
    10 use_thy "prime_def";
    10 use_thy "prime_def";
    11 use_thy "simp";
    11 use_thy "simp";
    12 use_thy "Itrev";
    12 use_thy "Itrev";
    13 use_thy "AdvancedInd";
    13 use_thy "AdvancedInd";
       
    14 use_thy "appendix";