diff -r 8f0b2daa7eaa -r d93ead9ac6df src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/AxExample.thy	Thu Jun 12 12:44:47 2025 +0200
@@ -127,7 +127,7 @@
 apply       (rule ax_subst_Var_allI)
 apply       (tactic \<open>inst1_tac \<^context> "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"]\<close>)
 apply       (rule allI)
-apply       (tactic \<open>simp_tac (\<^context> delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1\<close>)
+apply       (tactic \<open>simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac" |> Simplifier.del_simps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1\<close>)
 apply       (rule ax_derivs.Abrupt)
 apply      (simp (no_asm))
 apply      (tactic "ax_tac \<^context> 1" (* FVar *))
@@ -177,26 +177,26 @@
 apply  (rule ax_InitS)
 apply     force
 apply    (simp (no_asm))
-apply   (tactic \<open>simp_tac (\<^context> delloop "split_all_tac") 1\<close>)
+apply   (tactic \<open>simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\<close>)
 apply   (rule ax_Init_Skip_lemma)
-apply  (tactic \<open>simp_tac (\<^context> delloop "split_all_tac") 1\<close>)
+apply  (tactic \<open>simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\<close>)
 apply  (rule ax_InitS [THEN conseq1] (* init Base *))
 apply      force
 apply     (simp (no_asm))
 apply    (unfold arr_viewed_from_def)
 apply    (rule allI)
 apply    (rule_tac P' = "Normal P" and P = P for P in conseq1)
-apply     (tactic \<open>simp_tac (\<^context> delloop "split_all_tac") 1\<close>)
+apply     (tactic \<open>simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\<close>)
 apply     (tactic "ax_tac \<^context> 1")
 apply     (tactic "ax_tac \<^context> 1")
 apply     (rule_tac [2] ax_subst_Var_allI)
 apply      (tactic \<open>inst1_tac \<^context> "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"]\<close>)
-apply     (tactic \<open>simp_tac (\<^context> delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2\<close>)
+apply     (tactic \<open>simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac" |> Simplifier.del_simps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2\<close>)
 apply      (tactic "ax_tac \<^context> 2" (* NewA *))
 apply       (tactic "ax_tac \<^context> 3" (* ax_Alloc_Arr *))
 apply       (tactic "ax_tac \<^context> 3")
 apply      (tactic \<open>inst1_tac \<^context> "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"]\<close>)
-apply      (tactic \<open>simp_tac (\<^context> delloop "split_all_tac") 2\<close>)
+apply      (tactic \<open>simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 2\<close>)
 apply      (tactic "ax_tac \<^context> 2")
 apply     (tactic "ax_tac \<^context> 1" (* FVar *))
 apply      (tactic "ax_tac \<^context> 2" (* StatRef *))
@@ -207,7 +207,7 @@
 apply     (drule initedD)
 apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
 apply    force
-apply   (tactic \<open>simp_tac (\<^context> delloop "split_all_tac") 1\<close>)
+apply   (tactic \<open>simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\<close>)
 apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
 apply     (rule wf_tprg)
 apply    clarsimp