equal
deleted
inserted
replaced
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 |
34 with_path "Integ" use_thy "Main"; |
37 with_path "Integ" use_thy "Main"; |
35 |
38 |
36 path_add "~~/src/HOL/Library"; |
39 path_add "~~/src/HOL/Library"; |
37 |
40 |
38 Goal "True"; (*leave subgoal package empty*) |
41 Goal "True"; (*leave subgoal package empty*) |