Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/numeral_simprocs.ML
changeset 44984 6e6e958b2d40
parent 44947 8ae418dfe561
parent 44983 b36eedcd1633
child 45270 d5b5c9259afd 
--- a/src/HOL/Tools/numeral_simprocs.ML	Sun Sep 18 21:41:36 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Sun Sep 18 16:12:43 2011 -0700
@@ -367,9 +367,9 @@
   val dest_coeff = dest_coeff 1
   val trans_tac = 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