changeset 45306 | 1e380c50a183 |
parent 45284 | ae78a4ffa81d |
child 45437 | 958d19d3405b |
--- a/src/HOL/Tools/numeral_simprocs.ML Fri Oct 28 16:49:15 2011 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat Oct 29 10:00:35 2011 +0200 @@ -470,7 +470,6 @@ val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) val simplify_meta_eq = cancel_simplify_meta_eq - val prove_conv = Arith_Data.prove_conv fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) end;