src/HOL/Bali/AxExample.thy

 apply      (tactic "ax_tac \<^context> 1") (* Ass *)
 prefer 2
 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 *))
 apply       (tactic "ax_tac \<^context> 2", tactic "ax_tac \<^context> 2", tactic "ax_tac \<^context> 2")
 apply      (tactic "ax_tac \<^context> 1")

 apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
      (* begin init *)
 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 *))
 apply     (rule ax_derivs.Done [THEN conseq1])
 apply     (tactic \<open>inst1_tac \<^context> "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" []\<close>)
 apply     (clarsimp split del: if_split)
 apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
 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
 apply   (tactic \<open>inst1_tac \<^context> "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" []\<close>)
 apply   clarsimp