src/HOL/Integ/int_factor_simprocs.ML
changeset 18328 841261f303a1
parent 17877 67d5ab1cb0d8
child 18442 b35d7312c64f
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 01 22:03:06 2005 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Thu Dec 01 22:04:27 2005 +0100
     1.3 @@ -43,14 +43,17 @@
     1.4    val mk_coeff          = mk_coeff
     1.5    val dest_coeff        = dest_coeff 1
     1.6    val trans_tac         = fn _ => trans_tac
     1.7 +
     1.8 +  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
     1.9 +  val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps
    1.10 +  val norm_ss3 = HOL_ss addsimps mult_ac
    1.11    fun norm_tac ss =
    1.12 -    let val HOL_ss' = Simplifier.inherit_context ss HOL_ss in
    1.13 -      ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s))
    1.14 -      THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps))
    1.15 -      THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac))
    1.16 -    end
    1.17 -  fun numeral_simp_tac ss =
    1.18 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rel_number_of @ bin_simps))
    1.19 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.20 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
    1.21 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
    1.22 +
    1.23 +  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps
    1.24 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    1.25    val simplify_meta_eq = 
    1.26  	Int_Numeral_Simprocs.simplify_meta_eq
    1.27  	     [add_0, add_0_right,
    1.28 @@ -250,8 +253,8 @@
    1.29    val dest_coeff        = dest_coeff
    1.30    val find_first        = find_first []
    1.31    val trans_tac         = fn _ => trans_tac
    1.32 -  fun norm_tac ss =
    1.33 -    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
    1.34 +  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
    1.35 +  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
    1.36    end;
    1.37  
    1.38  (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in