src/HOL/ex/ROOT.ML
changeset 22522 783c8dbe3ade
parent 22505 e2d378a97905
child 22528 8501c4a62a3c
equal deleted inserted replaced
22521:8c000a2ea2f2 22522:783c8dbe3ade
     6 
     6 
     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 "CodeEval";
    11 no_document time_use_thy "Eval_examples";
    12 no_document time_use_thy "CodeRandom";
    12 no_document time_use_thy "CodeRandom";
    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";