merged
authorhuffman
Sun Sep 18 16:12:43 2011 -0700 (2011-09-18)
changeset 449846e6e958b2d40
parent 44982 e7ac11643bef
parent 44983 b36eedcd1633
child 44985 272e8e4e4fc7
child 44994 a915907a67d5
merged
src/HOL/Tools/numeral_simprocs.ML
     1.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sun Sep 18 21:41:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sun Sep 18 16:12:43 2011 -0700
     1.3 @@ -367,9 +367,9 @@
     1.4    val dest_coeff = dest_coeff 1
     1.5    val trans_tac = trans_tac
     1.6  
     1.7 -  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
     1.8 -  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
     1.9 -  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
    1.10 +  val norm_ss1 = HOL_basic_ss addsimps minus_from_mult_simps @ mult_1s
    1.11 +  val norm_ss2 = HOL_basic_ss addsimps simps @ mult_minus_simps
    1.12 +  val norm_ss3 = HOL_basic_ss addsimps @{thms mult_ac}
    1.13    fun norm_tac ss =
    1.14      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    1.15      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))