equal
deleted
inserted
replaced
359 |
359 |
360 (*Final simplification: cancel + and * *) |
360 (*Final simplification: cancel + and * *) |
361 val simplify_meta_eq = |
361 val simplify_meta_eq = |
362 Int_Numeral_Simprocs.simplify_meta_eq |
362 Int_Numeral_Simprocs.simplify_meta_eq |
363 [add_0, add_0_right, |
363 [add_0, add_0_right, |
364 mult_left_zero, mult_right_zero, mult_1, mult_1_right]; |
364 mult_zero_left, mult_zero_right, mult_1, mult_1_right]; |
365 |
365 |
366 fun prep_simproc (name, pats, proc) = |
366 fun prep_simproc (name, pats, proc) = |
367 Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc; |
367 Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc; |
368 |
368 |
369 structure CancelNumeralsCommon = |
369 structure CancelNumeralsCommon = |