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/nat_numeral_simprocs.ML
changeset 82967 73af47bc277c
parent 78800 0b3700d31758 
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -28,7 +28,7 @@
 (*Maps n to #n for n = 1, 2*)
 val numeral_syms = [@{thm numeral_One} RS sym, @{thm numeral_2_eq_2} RS sym];
 val numeral_sym_ss =
-  simpset_of (put_simpset HOL_basic_ss \<^context> addsimps numeral_syms);
+  simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps numeral_syms);
 
 (*Utilities*)
 
@@ -158,18 +158,18 @@
 
   val norm_ss1 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context>
-      addsimps numeral_syms @ add_0s @ mult_1s @
-        [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
+      |> Simplifier.add_simps (numeral_syms @ add_0s @ mult_1s @
+        [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps}))
   val norm_ss2 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context>
-      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
+      |> Simplifier.add_simps (bin_simps @ @{thms ac_simps} @ @{thms ac_simps}))
   fun norm_tac ctxt = 
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
 
   val numeral_simp_ss =
     simpset_of (put_simpset HOL_basic_ss \<^context>
-      addsimps add_0s @ bin_simps);
+      |> Simplifier.add_simps (add_0s @ bin_simps));
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt));
   val simplify_meta_eq  = simplify_meta_eq
@@ -231,17 +231,17 @@
 
   val norm_ss1 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context>
-      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms ac_simps})
+      |> Simplifier.add_simps (numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms ac_simps}))
   val norm_ss2 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context>
-      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
+      |> Simplifier.add_simps (bin_simps @ @{thms ac_simps} @ @{thms ac_simps}))
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
 
   val numeral_simp_ss =
     simpset_of (put_simpset HOL_basic_ss \<^context>
-      addsimps add_0s @ bin_simps);
+      |> Simplifier.add_simps (add_0s @ bin_simps));
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq = simplify_meta_eq
@@ -262,16 +262,17 @@
 
   val norm_ss1 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context>
-      addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps})
+      |> Simplifier.add_simps
+          (numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms ac_simps}))
   val norm_ss2 =
     simpset_of (put_simpset Numeral_Simprocs.num_ss \<^context>
-      addsimps bin_simps @ @{thms ac_simps} @ @{thms ac_simps})
+      |> Simplifier.add_simps (bin_simps @ @{thms ac_simps} @ @{thms ac_simps}))
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
 
   val numeral_simp_ss =
-    simpset_of (put_simpset HOL_basic_ss \<^context> addsimps bin_simps)
+    simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_simps bin_simps)
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq = simplify_meta_eq
@@ -357,7 +358,7 @@
   val trans_tac = Numeral_Simprocs.trans_tac
   val norm_ss =
     simpset_of (put_simpset HOL_basic_ss \<^context>
-      addsimps mult_1s @ @{thms ac_simps})
+      |> Simplifier.add_simps (mult_1s @ @{thms ac_simps}))
   fun norm_tac ctxt =
     ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
   val simplify_meta_eq  = cancel_simplify_meta_eq
isabelle