equal
deleted
inserted
replaced
41 structure CancelNumeralFactorCommon = |
41 structure CancelNumeralFactorCommon = |
42 struct |
42 struct |
43 val mk_coeff = mk_coeff |
43 val mk_coeff = mk_coeff |
44 val dest_coeff = dest_coeff 1 |
44 val dest_coeff = dest_coeff 1 |
45 val trans_tac = trans_tac |
45 val trans_tac = trans_tac |
46 val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s)) |
46 val norm_tac = |
47 THEN ALLGOALS |
47 ALLGOALS (simp_tac (HOL_ss addsimps mult_1s)) |
48 (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@ |
48 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) |
49 bin_simps@zmult_ac)) |
49 THEN ALLGOALS |
|
50 (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@zmult_ac)) |
50 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps)) |
51 val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps)) |
51 val simplify_meta_eq = simplify_meta_eq mult_1s |
52 val simplify_meta_eq = simplify_meta_eq mult_1s |
52 end |
53 end |
53 |
54 |
54 structure DivCancelNumeralFactor = CancelNumeralFactorFun |
55 structure DivCancelNumeralFactor = CancelNumeralFactorFun |