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 use_thy "mono"; |
|
25 use "ind_syntax.ML"; |
|
26 use_thy "Datatype"; |
|
27 |
|
28 use "Tools/numeral_syntax.ML"; |
|
29 (*the all-in-one theory*) |
|
30 with_path "Integ" use_thy "Main"; |
24 with_path "Integ" use_thy "Main"; |
31 |
|
32 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); |
33 |
26 |
34 print_depth 8; |
27 print_depth 8; |
35 |
28 |
36 Goal "True"; (*leave subgoal package empty*) |
29 Goal "True"; (*leave subgoal package empty*) |