equal
deleted
inserted
replaced
33 use "~~/src/Provers/Arith/cancel_numerals.ML"; |
33 use "~~/src/Provers/Arith/cancel_numerals.ML"; |
34 use "~~/src/Provers/Arith/combine_numerals.ML"; |
34 use "~~/src/Provers/Arith/combine_numerals.ML"; |
35 use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; |
35 use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; |
36 use "~~/src/Provers/Arith/extract_common_term.ML"; |
36 use "~~/src/Provers/Arith/extract_common_term.ML"; |
37 use "~~/src/Provers/Arith/cancel_div_mod.ML"; |
37 use "~~/src/Provers/Arith/cancel_div_mod.ML"; |
|
38 use "~~/src/Provers/linorder.ML"; |
38 |
39 |
39 with_path "Integ" use_thy "Main"; |
40 with_path "Integ" use_thy "Main"; |
40 |
41 |
41 path_add "~~/src/HOL/Library"; |
42 path_add "~~/src/HOL/Library"; |
42 |
43 |