equal
deleted
inserted
replaced
19 use "thy_syntax"; |
19 use "thy_syntax"; |
20 |
20 |
21 use "~~/src/Provers/Arith/cancel_numerals.ML"; |
21 use "~~/src/Provers/Arith/cancel_numerals.ML"; |
22 use "~~/src/Provers/Arith/combine_numerals.ML"; |
22 use "~~/src/Provers/Arith/combine_numerals.ML"; |
23 |
23 |
24 with_path "Integ" use_thy "Main"; |
24 with_path "Integ" use_thy "Main_ZFC"; |
25 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all); |
25 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all); |
26 |
26 |
27 print_depth 8; |
27 print_depth 8; |
28 |
28 |
29 Goal "True"; (*leave subgoal package empty*) |
29 Goal "True"; (*leave subgoal package empty*) |