src/HOL/Induct/ROOT.ML
changeset 7019 71f2155cdd85
parent 6349 f7750d816c21
child 8917 2ff6f8693c4f
equal deleted inserted replaced
7018:ae18bb3075c3 7019:71f2155cdd85
    18 time_use_thy "SList";
    18 time_use_thy "SList";
    19 time_use_thy "LFilter";
    19 time_use_thy "LFilter";
    20 time_use_thy "Term";
    20 time_use_thy "Term";
    21 time_use_thy "ABexp";
    21 time_use_thy "ABexp";
    22 time_use_thy "Exp";
    22 time_use_thy "Exp";
       
    23 time_use_thy "Tree";