src/ZF/int_arith.ML

--- a/src/ZF/int_arith.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/ZF/int_arith.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -157,13 +157,13 @@
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss \<^context>
-      addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac})
+      |> Simplifier.add_simps (add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}))
   val norm_ss2 =
     simpset_of (put_simpset ZF_ss \<^context>
-      addsimps bin_simps @ int_mult_minus_simps @ intifys)
+      |> Simplifier.add_simps (bin_simps @ int_mult_minus_simps @ intifys))
   val norm_ss3 =
     simpset_of (put_simpset ZF_ss \<^context>
-      addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)
+      |> Simplifier.add_simps (int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys))
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
@@ -171,7 +171,7 @@
 
   val numeral_simp_ss =
     simpset_of (put_simpset ZF_ss \<^context>
-      addsimps add_0s @ bin_simps @ tc_rules @ intifys)
+      |> Simplifier.add_simps (add_0s @ bin_simps @ tc_rules @ intifys))
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
     THEN ALLGOALS (asm_simp_tac ctxt)
@@ -229,20 +229,20 @@
 
   val norm_ss1 =
     simpset_of (put_simpset ZF_ss \<^context>
-      addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys)
+      |> Simplifier.add_simps (add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys))
   val norm_ss2 =
     simpset_of (put_simpset ZF_ss \<^context>
-      addsimps bin_simps @ int_mult_minus_simps @ intifys)
+      |> Simplifier.add_simps (bin_simps @ int_mult_minus_simps @ intifys))
   val norm_ss3 =
     simpset_of (put_simpset ZF_ss \<^context>
-      addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys)
+      |> Simplifier.add_simps (int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys))
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss3 ctxt))
 
   val numeral_simp_ss =
-    simpset_of (put_simpset ZF_ss \<^context> addsimps add_0s @ bin_simps @ tc_rules @ intifys)
+    simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (add_0s @ bin_simps @ tc_rules @ intifys))
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
@@ -275,16 +275,16 @@
   fun trans_tac ctxt = ArithData.gen_trans_tac ctxt @{thm trans}
 
   val norm_ss1 =
-    simpset_of (put_simpset ZF_ss \<^context> addsimps mult_1s @ diff_simps @ zminus_simps)
+    simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (mult_1s @ diff_simps @ zminus_simps))
   val norm_ss2 =
-    simpset_of (put_simpset ZF_ss \<^context> addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
-    bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys)
+    simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps ([@{thm zmult_zminus_right} RS @{thm sym}] @
+    bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys))
   fun norm_tac ctxt =
     ALLGOALS (asm_simp_tac (put_simpset norm_ss1 ctxt))
     THEN ALLGOALS (asm_simp_tac (put_simpset norm_ss2 ctxt))
 
   val numeral_simp_ss =
-    simpset_of (put_simpset ZF_ss \<^context> addsimps bin_simps @ tc_rules @ intifys)
+    simpset_of (put_simpset ZF_ss \<^context> |> Simplifier.add_simps (bin_simps @ tc_rules @ intifys))
   fun numeral_simp_tac ctxt =
     ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
   val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);