src/HOL/ex/ROOT.ML
changeset 31555 318081898306
parent 31381 b3a785a69538
child 31556 ac0badf13d93
equal deleted inserted replaced
31554:a6c6bf2751a0 31555:318081898306
    12   "Quickcheck_Generators",
    12   "Quickcheck_Generators",
    13   "Codegenerator_Test",
    13   "Codegenerator_Test",
    14   "Codegenerator_Pretty_Test",
    14   "Codegenerator_Pretty_Test",
    15   "NormalForm",
    15   "NormalForm",
    16   "../NumberTheory/Factorization",
    16   "../NumberTheory/Factorization",
    17   "Predicate_Compile",
    17   "Predicate_Compile"
    18   "Predicate_Compile_ex"
       
    19 ];
    18 ];
       
    19 
       
    20 setmp quick_and_dirty true use_thy "Predicate_Compile_ex";
    20 
    21 
    21 use_thys [
    22 use_thys [
    22   "Numeral",
    23   "Numeral",
    23   "Higher_Order_Logic",
    24   "Higher_Order_Logic",
    24   "Abstract_NAT",
    25   "Abstract_NAT",