src/HOL/ex/ROOT.ML
changeset 31129 d2cead76fca2
parent 30740 2d3ae5a7edb2
child 31181 27304e12a412
equal deleted inserted replaced
31128:b3bb28c87409 31129:d2cead76fca2
    14   "Term_Of_Syntax",
    14   "Term_Of_Syntax",
    15   "Codegenerator",
    15   "Codegenerator",
    16   "Codegenerator_Pretty",
    16   "Codegenerator_Pretty",
    17   "NormalForm",
    17   "NormalForm",
    18   "../NumberTheory/Factorization",
    18   "../NumberTheory/Factorization",
    19   "Predicate_Compile"
    19   "Predicate_Compile",
       
    20   "Predicate_Compile_ex"
    20 ];
    21 ];
    21 
    22 
    22 use_thys [
    23 use_thys [
    23   "Numeral",
    24   "Numeral",
    24   "Higher_Order_Logic",
    25   "Higher_Order_Logic",