src/HOL/Integ/int_factor_simprocs.ML
changeset 14113 7b3513ba0f86
parent 13485 acf39e924091
child 14378 69c4d5997669
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Jul 15 15:12:22 2003 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Jul 15 15:20:54 2003 +0200
     1.3 @@ -46,8 +46,7 @@
     1.4    val norm_tac =
     1.5       ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
     1.6       THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
     1.7 -     THEN ALLGOALS
     1.8 -            (simp_tac (HOL_ss addsimps zmult_ac))
     1.9 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps zmult_ac))
    1.10    val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.11    val simplify_meta_eq  = simplify_meta_eq mult_1s
    1.12    end