src/HOL/Integ/int_factor_simprocs.ML
changeset 10713 69c9fc1d11f2
parent 10703 ba98f00cec4f
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Wed Dec 20 12:15:52 2000 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 21 10:11:10 2000 +0100
     1.3 @@ -43,10 +43,11 @@
     1.4    val mk_coeff		= mk_coeff
     1.5    val dest_coeff	= dest_coeff 1
     1.6    val trans_tac         = trans_tac
     1.7 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
     1.8 -                 THEN ALLGOALS
     1.9 -                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
    1.10 -                                               bin_simps@zmult_ac))
    1.11 +  val norm_tac = 
    1.12 +     ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
    1.13 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    1.14 +     THEN ALLGOALS
    1.15 +            (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@zmult_ac))
    1.16    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.17    val simplify_meta_eq  = simplify_meta_eq mult_1s
    1.18    end