src/HOL/ROOT.ML
changeset 10689 5c44de6aadf4
parent 10535 c00b1d0d46ac
child 10766 ace2ba2d4fd1
equal deleted inserted replaced
10688:4cf4bbc25267 10689:5c44de6aadf4
    32 use "~~/src/Provers/Arith/assoc_fold.ML";
    32 use "~~/src/Provers/Arith/assoc_fold.ML";
    33 use "~~/src/Provers/quantifier1.ML";
    33 use "~~/src/Provers/quantifier1.ML";
    34 use "~~/src/Provers/Arith/cancel_numerals.ML";
    34 use "~~/src/Provers/Arith/cancel_numerals.ML";
    35 use "~~/src/Provers/Arith/combine_numerals.ML";
    35 use "~~/src/Provers/Arith/combine_numerals.ML";
    36 use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
    36 use "~~/src/Provers/Arith/cancel_numeral_factor.ML";
       
    37 use "~~/src/Provers/Arith/extract_common_term.ML";
    37 
    38 
    38 with_path "Integ" use_thy "Main";
    39 with_path "Integ" use_thy "Main";
    39 
    40 
    40 path_add "~~/src/HOL/Library";
    41 path_add "~~/src/HOL/Library";
    41 
    42