src/HOL/ex/ROOT.ML
changeset 22528 8501c4a62a3c
parent 22522 783c8dbe3ade
child 22657 731622340817
equal deleted inserted replaced
22527:84690fcd3db9 22528:8501c4a62a3c
     7 no_document use_thy "Parity";
     7 no_document use_thy "Parity";
     8 no_document use_thy "GCD";
     8 no_document use_thy "GCD";
     9 
     9 
    10 no_document time_use_thy "Classpackage";
    10 no_document time_use_thy "Classpackage";
    11 no_document time_use_thy "Eval_examples";
    11 no_document time_use_thy "Eval_examples";
    12 no_document time_use_thy "CodeRandom";
    12 no_document time_use_thy "Random";
    13 no_document time_use_thy "Codegenerator_Rat";
    13 no_document time_use_thy "Codegenerator_Rat";
    14 no_document time_use_thy "Codegenerator";
    14 no_document time_use_thy "Codegenerator";
    15 
    15 
    16 time_use_thy "Higher_Order_Logic";
    16 time_use_thy "Higher_Order_Logic";
    17 time_use_thy "Abstract_NAT";
    17 time_use_thy "Abstract_NAT";