--- a/NEWS Thu Jun 12 08:03:05 2025 +0200
+++ b/NEWS Thu Jun 12 12:44:47 2025 +0200
@@ -279,6 +279,21 @@
etc.
+*** ML ***
+
+* Some old infix operations have been removed. INCOMPATIBILITY. The
+subsequent replacements have slightly different syntactic precedence and
+may require change of parentheses:
+
+ setloop |> Simplifier.set_loop
+ addloop |> Simplifier.add_loop
+ delloop |> Simplifier.del_loop
+ setSSolver |> Simplifier.set_safe_solver
+ addSSolver |> Simplifier.add_safe_solver
+ setSolver |> Simplifier.set_unsafe_solver
+ addSolver |> Simplifier.add_unsafe_solver
+
+
*** System ***
* System option "record_theories" tells "isabelle build" to record
--- a/src/CCL/Term.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/CCL/Term.thy Thu Jun 12 12:44:47 2025 +0200
@@ -202,10 +202,12 @@
method_setup beta_rl = \<open>
Scan.succeed (fn ctxt =>
- let val ctxt' = Context_Position.set_visible false ctxt in
- SIMPLE_METHOD' (CHANGED o
- simp_tac (ctxt' addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB})))
- end)
+ let
+ val ctxt' = ctxt
+ |> Context_Position.set_visible false
+ |> Simplifier.add_simps @{thms rawBs}
+ |> Simplifier.set_loop (fn _ => stac ctxt @{thm letrecB});
+ in SIMPLE_METHOD' (CHANGED o simp_tac ctxt') end)
\<close>
lemma ifBtrue: "if true then t else u = t"
--- a/src/FOL/simpdata.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/FOL/simpdata.ML Thu Jun 12 12:44:47 2025 +0200
@@ -125,8 +125,8 @@
(*No simprules, but basic infastructure for simplification*)
val FOL_basic_ss =
empty_simpset \<^context>
- setSSolver (mk_solver "FOL safe" safe_solver)
- setSolver (mk_solver "FOL unsafe" unsafe_solver)
+ |> Simplifier.set_safe_solver (mk_solver "FOL safe" safe_solver)
+ |> Simplifier.set_unsafe_solver (mk_solver "FOL unsafe" unsafe_solver)
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps mksimps_pairs)
|> Simplifier.set_mkcong mk_meta_cong
--- a/src/HOL/Auth/Public.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Auth/Public.thy Thu Jun 12 12:44:47 2025 +0200
@@ -414,7 +414,7 @@
(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (ctxt setSolver safe_solver delsimps [@{thm used_Says}]))
+ (ALLGOALS (simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver |> Simplifier.del_simp @{thm used_Says}))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}]))
@@ -423,7 +423,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
--- a/src/HOL/Auth/Shared.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Auth/Shared.thy Thu Jun 12 12:44:47 2025 +0200
@@ -202,7 +202,7 @@
(REPEAT
(ALLGOALS (simp_tac (ctxt
delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}]
- setSolver safe_solver))
+ |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}])))
@@ -211,7 +211,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jun 12 12:44:47 2025 +0200
@@ -368,7 +368,7 @@
(REPEAT
(ALLGOALS (simp_tac (ctxt
delsimps @{thms used_Cons_simps}
- setSolver safe_solver))
+ |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}])))
@@ -377,7 +377,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
--- 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
--- a/src/HOL/Bali/AxSem.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/AxSem.thy Thu Jun 12 12:44:47 2025 +0200
@@ -468,7 +468,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
inductive
--- a/src/HOL/Bali/Basis.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/Basis.thy Thu Jun 12 12:44:47 2025 +0200
@@ -12,7 +12,7 @@
ML \<open>fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\<close>
declare if_split_asm [split] option.split [split] option.split_asm [split]
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
declare if_weak_cong [cong del] option.case_cong_weak [cong del]
declare length_Suc_conv [iff]
--- a/src/HOL/Bali/DefiniteAssignment.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Thu Jun 12 12:44:47 2025 +0200
@@ -809,7 +809,7 @@
declare inj_term_sym_simps [simp]
declare assigns_if.simps [simp del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
inductive_cases da_elim_cases [cases set]:
"Env\<turnstile> B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A"
@@ -875,7 +875,7 @@
declare inj_term_sym_simps [simp del]
declare assigns_if.simps [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
(* To be able to eliminate both the versions with the overloaded brackets:
(B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A),
--- a/src/HOL/Bali/Eval.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/Eval.thy Thu Jun 12 12:44:47 2025 +0200
@@ -774,7 +774,7 @@
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
@@ -812,7 +812,7 @@
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<rightarrow> (x, s')"
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *)
declare split_paired_All [simp] split_paired_Ex [simp]
-declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
+declaration \<open>K (Simplifier.map_ss (fn ss => ss |> Simplifier.add_loop ("split_all_tac", split_all_tac)))\<close>
declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
--- a/src/HOL/Bali/Evaln.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/Evaln.thy Thu Jun 12 12:44:47 2025 +0200
@@ -197,7 +197,7 @@
option.split [split del] option.split_asm [split del]
not_None_eq [simp del]
split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
@@ -238,7 +238,7 @@
option.split [split] option.split_asm [split]
not_None_eq [simp]
split_paired_All [simp] split_paired_Ex [simp]
-declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
+declaration \<open>K (Simplifier.map_ss (fn ss => ss |> Simplifier.add_loop ("split_all_tac", split_all_tac)))\<close>
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>
(case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)
--- a/src/HOL/Bali/TypeSafe.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Thu Jun 12 12:44:47 2025 +0200
@@ -726,7 +726,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
lemma FVar_lemma:
@@ -756,7 +756,7 @@
declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i;
@@ -871,7 +871,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
lemma conforms_init_lvars:
@@ -925,7 +925,7 @@
declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
subsection "accessibility"
--- a/src/HOL/Bali/WellForm.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/WellForm.thy Thu Jun 12 12:44:47 2025 +0200
@@ -2125,7 +2125,7 @@
qed
declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
lemma dynamic_mheadsD:
@@ -2256,7 +2256,7 @@
qed
declare split_paired_All [simp] split_paired_Ex [simp]
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
(* Tactical version *)
(*
@@ -2399,7 +2399,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow> wf_prog (prg E) \<longrightarrow>
@@ -2425,7 +2425,7 @@
done
declare split_paired_All [simp] split_paired_Ex [simp]
setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
lemma ty_expr_is_type:
"\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
--- a/src/HOL/Bali/WellType.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/WellType.thy Thu Jun 12 12:44:47 2025 +0200
@@ -455,7 +455,7 @@
declare not_None_eq [simp del]
declare if_split [split del] if_split_asm [split del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
inductive_cases wt_elim_cases [cases set]:
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T"
@@ -491,7 +491,7 @@
declare not_None_eq [simp]
declare if_split [split] if_split_asm [split]
declare split_paired_All [simp] split_paired_Ex [simp]
-setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\<close>
lemma is_acc_class_is_accessible:
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
--- a/src/HOL/Orderings.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Orderings.thy Thu Jun 12 12:44:47 2025 +0200
@@ -653,8 +653,8 @@
end
setup \<open>
- map_theory_simpset (fn ctxt0 => ctxt0 addSolver
- mk_solver "partial and linear orders" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt))
+ map_theory_simpset (fn ctxt0 => ctxt0 |> Simplifier.add_unsafe_solver
+ (mk_solver "partial and linear orders" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt)))
\<close>
ML \<open>
--- a/src/HOL/SET_Protocol/Public_SET.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy Thu Jun 12 12:44:47 2025 +0200
@@ -353,7 +353,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver))
THEN
REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
\<close>
--- a/src/HOL/Statespace/state_fun.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Statespace/state_fun.ML Thu Jun 12 12:44:47 2025 +0200
@@ -92,7 +92,7 @@
@ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
@{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
|> Simplifier.add_proc lazy_conj_simproc)
- addSolver StateSpace.distinctNameSolver
+ |> Simplifier.add_unsafe_solver StateSpace.distinctNameSolver
|> fold Simplifier.add_cong @{thms block_conj_cong});
val ex_lookup_ss =
--- a/src/HOL/TLA/Action.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/TLA/Action.thy Thu Jun 12 12:44:47 2025 +0200
@@ -260,7 +260,7 @@
*)
fun action_simp_tac ctxt intros elims =
asm_full_simp_tac
- (ctxt setloop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros)
+ (ctxt |> Simplifier.set_loop (fn _ => (resolve_tac ctxt ((map (action_use ctxt) intros)
@ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims)
@ [conjE,disjE,exE]))));
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 12 12:44:47 2025 +0200
@@ -231,7 +231,7 @@
else K no_tac);
\<close>
-setup \<open>map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver)\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_safe_solver fast_solver)\<close>
ML \<open>val temp_elim = make_elim oo temp_use\<close>
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Jun 12 12:44:47 2025 +0200
@@ -36,8 +36,8 @@
val HOL_basic_ss' =
simpset_of (put_simpset HOL_basic_ss \<^context>
addsimps @{thms simp_thms prod.inject}
- setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
- setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
+ |> Simplifier.set_unsafe_solver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
+ |> Simplifier.set_unsafe_solver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
(* auxillary functions *)
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 12 12:44:47 2025 +0200
@@ -152,7 +152,8 @@
(mk_minimal_simpset ctxt
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
|> Simplifier.add_proc regularize_simproc)
- addSolver equiv_solver addSolver quotient_solver
+ |> Simplifier.add_unsafe_solver equiv_solver
+ |> Simplifier.add_unsafe_solver quotient_solver
val eq_eqvs = eq_imp_rel_get ctxt
in
simp_tac simpset THEN'
@@ -509,7 +510,9 @@
val thms =
@{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
- val simpset = (mk_minimal_simpset ctxt) addsimps thms addSolver quotient_solver
+ val simpset =
+ (mk_minimal_simpset ctxt) addsimps thms
+ |> Simplifier.add_unsafe_solver quotient_solver
in
EVERY' [
map_fun_tac ctxt,
--- a/src/HOL/Tools/lin_arith.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Jun 12 12:44:47 2025 +0200
@@ -946,7 +946,7 @@
val global_setup =
map_theory_simpset (fn ctxt => ctxt
- addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #>
+ |> Simplifier.add_unsafe_solver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #>
Attrib.setup \<^binding>\<open>linarith_split\<close> (Scan.succeed (Thm.declaration_attribute add_split))
"declaration of split rules for arithmetic procedure" #>
Method.setup \<^binding>\<open>linarith\<close>
--- a/src/HOL/Tools/simpdata.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Tools/simpdata.ML Thu Jun 12 12:44:47 2025 +0200
@@ -186,8 +186,8 @@
val HOL_basic_ss =
empty_simpset \<^context>
- setSSolver safe_solver
- setSolver unsafe_solver
+ |> Simplifier.set_safe_solver safe_solver
+ |> Simplifier.set_unsafe_solver unsafe_solver
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (mksimps mksimps_pairs)
|> Simplifier.set_mkeqTrue mk_eq_True
--- a/src/HOL/Transitive_Closure.thy Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Jun 12 12:44:47 2025 +0200
@@ -1581,10 +1581,10 @@
setup \<open>
map_theory_simpset (fn ctxt => ctxt
- addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac)
- addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac)
- addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac)
- addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac))
+ |> Simplifier.add_unsafe_solver (mk_solver "Trancl" Trancl_Tac.trancl_tac)
+ |> Simplifier.add_unsafe_solver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac)
+ |> Simplifier.add_unsafe_solver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac)
+ |> Simplifier.add_unsafe_solver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac))
\<close>
lemma transp_rtranclp [simp]: "transp R\<^sup>*\<^sup>*"
--- a/src/Sequents/simpdata.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/Sequents/simpdata.ML Thu Jun 12 12:44:47 2025 +0200
@@ -68,8 +68,8 @@
(*No simprules, but basic infrastructure for simplification*)
val LK_basic_ss =
empty_simpset \<^context>
- setSSolver (mk_solver "safe" safe_solver)
- setSolver (mk_solver "unsafe" unsafe_solver)
+ |> Simplifier.set_safe_solver (mk_solver "safe" safe_solver)
+ |> Simplifier.set_unsafe_solver (mk_solver "unsafe" unsafe_solver)
|> Simplifier.set_subgoaler asm_simp_tac
|> Simplifier.set_mksimps (fn ctxt => map (mk_meta_eq ctxt) o atomize o Variable.gen_all ctxt)
|> Simplifier.set_mkcong mk_meta_cong
--- a/src/Tools/simp_legacy.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/Tools/simp_legacy.ML Thu Jun 12 12:44:47 2025 +0200
@@ -3,31 +3,10 @@
Legacy simplifier configuration interfaces -- to be phased out eventually.
*)
-infix 4
- addsimps delsimps addsimprocs delsimprocs
- setloop addloop delloop
- setSSolver addSSolver setSolver addSolver;
-
-local
-
-open Simplifier
-
-in
-
-fun ctxt addsimps thms = ctxt |> add_simps thms;
-fun ctxt delsimps thms = ctxt |> del_simps thms;
+infix 4 addsimps delsimps addsimprocs delsimprocs;
-fun ctxt addsimprocs procs = ctxt |> fold add_proc procs;
-fun ctxt delsimprocs procs = ctxt |> fold del_proc procs;
-
-fun ctxt setloop looper = ctxt |> set_loop looper;
-fun ctxt addloop looper = ctxt |> add_loop looper;
-fun ctxt delloop looper = ctxt |> del_loop looper;
+fun ctxt addsimps thms = ctxt |> Simplifier.add_simps thms;
+fun ctxt delsimps thms = ctxt |> Simplifier.del_simps thms;
-fun ctxt setSSolver solver = ctxt |> set_safe_solver solver;
-fun ctxt addSSolver solver = ctxt |> add_safe_solver solver;
-
-fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver;
-fun ctxt addSolver solver = ctxt |> add_unsafe_solver solver;
-
-end
+fun ctxt addsimprocs procs = ctxt |> fold Simplifier.add_proc procs;
+fun ctxt delsimprocs procs = ctxt |> fold Simplifier.del_proc procs;
--- a/src/ZF/Tools/inductive_package.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu Jun 12 12:44:47 2025 +0200
@@ -341,9 +341,9 @@
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
If the premises get simplified, then the proofs could fail.*)
val min_ss =
- (empty_simpset ctxt4
- |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt))
- setSolver (mk_solver "minimal"
+ empty_simpset ctxt4
+ |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
+ |> Simplifier.set_unsafe_solver (mk_solver "minimal"
(fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
ORELSE' assume_tac ctxt
ORELSE' eresolve_tac ctxt @{thms FalseE}));
--- a/src/ZF/Tools/typechk.ML Thu Jun 12 08:03:05 2025 +0200
+++ b/src/ZF/Tools/typechk.ML Thu Jun 12 12:44:47 2025 +0200
@@ -107,7 +107,8 @@
Simplifier.mk_solver "ZF typecheck" (fn ctxt =>
type_solver_tac ctxt (Simplifier.prems_of ctxt));
-val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt setSolver type_solver));
+val _ =
+ Theory.setup (map_theory_simpset (fn ctxt => ctxt |> Simplifier.set_unsafe_solver type_solver));
(* concrete syntax *)