changeset 58838 | 59203adfc33f |
parent 51717 | 9e7d1c139569 |
child 59498 | 50b60f501b05 |
--- a/src/Provers/Arith/combine_numerals.ML Thu Oct 30 16:20:46 2014 +0100 +++ b/src/Provers/Arith/combine_numerals.ML Thu Oct 30 16:55:29 2014 +0100 @@ -83,7 +83,7 @@ in Option.map (export o Data.simplify_meta_eq ctxt) (Data.prove_conv - [Data.trans_tac reshape, rtac Data.left_distrib 1, + [Data.trans_tac reshape, resolve_tac [Data.left_distrib] 1, Data.numeral_simp_tac ctxt] ctxt (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) end