src/HOL/ROOT.ML
changeset 19174 df9de25e87b3
parent 19161 b395f586633f
child 19835 81d6dc597559
equal deleted inserted replaced
19173:fee0e93efa78 19174:df9de25e87b3
    29 use "~~/src/Provers/Arith/extract_common_term.ML";
    29 use "~~/src/Provers/Arith/extract_common_term.ML";
    30 use "~~/src/Provers/Arith/cancel_div_mod.ML";
    30 use "~~/src/Provers/Arith/cancel_div_mod.ML";
    31 use "~~/src/Provers/quasi.ML";
    31 use "~~/src/Provers/quasi.ML";
    32 use "~~/src/Provers/order.ML";
    32 use "~~/src/Provers/order.ML";
    33 
    33 
    34 
       
    35 use "Tools/res_atpset.ML";
       
    36 
       
    37 with_path "Integ" use_thy "Main";
    34 with_path "Integ" use_thy "Main";
    38 
    35 
    39 path_add "~~/src/HOL/Library";
    36 path_add "~~/src/HOL/Library";
    40 
    37 
    41 Goal "True";  (*leave subgoal package empty*)
    38 Goal "True";  (*leave subgoal package empty*)