# HG changeset patch # User huffman # Date 1316106756 25200 # Node ID b36eedcd163302e1c9abc6b0b1b918ff9c916169 # Parent e1139e612b5551c39b3d957d58352d8fff4fe1ec numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else diff -r e1139e612b55 -r b36eedcd1633 src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Thu Sep 15 17:06:00 2011 +0200 +++ b/src/HOL/Tools/numeral_simprocs.ML Thu Sep 15 10:12:36 2011 -0700 @@ -361,9 +361,9 @@ val dest_coeff = dest_coeff 1 fun trans_tac _ = Arith_Data.trans_tac - val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s - val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps - val norm_ss3 = HOL_ss addsimps @{thms mult_ac} + val norm_ss1 = HOL_basic_ss addsimps minus_from_mult_simps @ mult_1s + val norm_ss2 = HOL_basic_ss addsimps simps @ mult_minus_simps + val norm_ss3 = HOL_basic_ss addsimps @{thms mult_ac} fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))