changeset 45270 | d5b5c9259afd |
parent 44984 | 6e6e958b2d40 |
child 45284 | ae78a4ffa81d |
--- a/src/HOL/Tools/numeral_simprocs.ML Tue Oct 25 16:37:11 2011 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Thu Oct 27 07:46:57 2011 +0200 @@ -512,6 +512,7 @@ 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; (*mult_cancel_left requires a ring with no zero divisors.*)