Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
authorhuffman
Thu, 15 Sep 2011 10:12:36 -0700
changeset 44983 b36eedcd1633
parent 44936 e1139e612b55
child 44984 6e6e958b2d40
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
src/HOL/Tools/numeral_simprocs.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle