src/HOL/Integ/int_factor_simprocs.ML
changeset 12018 ec054019c910
parent 11868 56db9f3a6b3e
child 13462 56610e2ba220
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Nov 01 21:12:13 2001 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Fri Nov 02 17:55:24 2001 +0100
     1.3 @@ -44,10 +44,10 @@
     1.4    val dest_coeff	= dest_coeff 1
     1.5    val trans_tac         = trans_tac
     1.6    val norm_tac = 
     1.7 -     ALLGOALS (simp_tac (HOL_ss addsimps mult_1s))
     1.8 +     ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
     1.9       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
    1.10       THEN ALLGOALS
    1.11 -            (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@zmult_ac))
    1.12 +            (simp_tac (HOL_ss addsimps zmult_ac))
    1.13    val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.14    val simplify_meta_eq  = simplify_meta_eq mult_1s
    1.15    end