# HG changeset patch # User wenzelm # Date 1749740068 -7200 # Node ID c0f166b39a3af71993a5dd1a6959958dab627678 # Parent 39a17ff4dd762fdc8e4e5c9ea75438dd057d7d77# Parent cc05bc2cfb2f23106ecef0c06b822b7809287d84 merged diff -r 39a17ff4dd76 -r c0f166b39a3a NEWS --- a/NEWS Thu Jun 12 10:38:02 2025 +0200 +++ b/NEWS Thu Jun 12 16:54:28 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 diff -r 39a17ff4dd76 -r c0f166b39a3a src/CCL/Term.thy --- a/src/CCL/Term.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/CCL/Term.thy Thu Jun 12 16:54:28 2025 +0200 @@ -202,10 +202,12 @@ method_setup beta_rl = \ 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) \ lemma ifBtrue: "if true then t else u = t" diff -r 39a17ff4dd76 -r c0f166b39a3a src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/FOL/IFOL.thy Thu Jun 12 16:54:28 2025 +0200 @@ -9,7 +9,6 @@ abbrevs "?<" = "\\<^sub>\\<^sub>1" begin -ML_file \~~/src/Tools/simp_legacy.ML\ ML_file \~~/src/Tools/misc_legacy.ML\ ML_file \~~/src/Provers/splitter.ML\ ML_file \~~/src/Provers/hypsubst.ML\ diff -r 39a17ff4dd76 -r c0f166b39a3a src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/FOL/simpdata.ML Thu Jun 12 16:54:28 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 diff -r 39a17ff4dd76 -r c0f166b39a3a src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/FOLP/IFOLP.thy Thu Jun 12 16:54:28 2025 +0200 @@ -9,7 +9,6 @@ imports Pure begin -ML_file \~~/src/Tools/simp_legacy.ML\ ML_file \~~/src/Tools/misc_legacy.ML\ setup Pure_Thy.old_appl_syntax_setup diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Auth/Public.thy Thu Jun 12 16:54:28 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])) diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Auth/Shared.thy Thu Jun 12 16:54:28 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])) diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jun 12 16:54:28 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])) diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/AxExample.thy Thu Jun 12 16:54:28 2025 +0200 @@ -127,7 +127,7 @@ apply (rule ax_subst_Var_allI) apply (tactic \inst1_tac \<^context> "P'" "\a vs l vf. PP a vs l vf\x \. p" ["PP", "x", "p"]\) apply (rule allI) -apply (tactic \simp_tac (\<^context> delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1\) +apply (tactic \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\) 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 \simp_tac (\<^context> delloop "split_all_tac") 1\) +apply (tactic \simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\) apply (rule ax_Init_Skip_lemma) -apply (tactic \simp_tac (\<^context> delloop "split_all_tac") 1\) +apply (tactic \simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\) 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 \simp_tac (\<^context> delloop "split_all_tac") 1\) +apply (tactic \simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\) apply (tactic "ax_tac \<^context> 1") apply (tactic "ax_tac \<^context> 1") apply (rule_tac [2] ax_subst_Var_allI) apply (tactic \inst1_tac \<^context> "P'" "\vf l vfa. Normal (P vf l vfa)" ["P"]\) -apply (tactic \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\) +apply (tactic \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\) apply (tactic "ax_tac \<^context> 2" (* NewA *)) apply (tactic "ax_tac \<^context> 3" (* ax_Alloc_Arr *)) apply (tactic "ax_tac \<^context> 3") apply (tactic \inst1_tac \<^context> "P" "\vf l vfa. Normal (P vf l vfa\\)" ["P"]\) -apply (tactic \simp_tac (\<^context> delloop "split_all_tac") 2\) +apply (tactic \simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 2\) 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 \simp_tac (\<^context> delloop "split_all_tac") 1\) +apply (tactic \simp_tac (\<^context> |> Simplifier.del_loop "split_all_tac") 1\) apply (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1]) apply (rule wf_tprg) apply clarsimp diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/AxSem.thy Thu Jun 12 16:54:28 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ inductive diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/Basis.thy Thu Jun 12 16:54:28 2025 +0200 @@ -12,7 +12,7 @@ ML \fun strip_tac ctxt i = REPEAT (resolve_tac ctxt [impI, allI] i)\ declare if_split_asm [split] option.split [split] option.split_asm [split] -setup \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\ declare if_weak_cong [cong del] option.case_cong_weak [cong del] declare length_Suc_conv [iff] diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/DefiniteAssignment.thy --- a/src/HOL/Bali/DefiniteAssignment.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/DefiniteAssignment.thy Thu Jun 12 16:54:28 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ inductive_cases da_elim_cases [cases set]: "Env\ B \\Skip\\ 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 \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\ (* To be able to eliminate both the versions with the overloaded brackets: (B \\Skip\\ A) and with the explicit constructor (B \In1r Skip\ A), diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/Eval.thy Thu Jun 12 16:54:28 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ inductive_cases eval_cases: "G\s \t\\ (v, s')" @@ -812,7 +812,7 @@ "G\Norm s \In1r (Init C) \\ (x, s')" declare not_None_eq [simp] (* IntDef.Zero_def [simp] *) declare split_paired_All [simp] split_paired_Ex [simp] -declaration \K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\ +declaration \K (Simplifier.map_ss (fn ss => ss |> Simplifier.add_loop ("split_all_tac", split_all_tac)))\ declare if_split [split] if_split_asm [split] option.split [split] option.split_asm [split] diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/Evaln.thy Thu Jun 12 16:54:28 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ inductive_cases evaln_cases: "G\s \t\\n\ (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 \K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\ +declaration \K (Simplifier.map_ss (fn ss => ss |> Simplifier.add_loop ("split_all_tac", split_all_tac)))\ lemma evaln_Inj_elim: "G\s \t\\n\ (w,s') \ case t of In1 ec \ (case ec of Inl e \ (\v. w = In1 v) | Inr c \ w = \) diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/TypeSafe.thy Thu Jun 12 16:54:28 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ lemma FVar_lemma: @@ -756,7 +756,7 @@ declare if_split [split] if_split_asm [split] option.split [split] option.split_asm [split] setup \map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\ -setup \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\ lemma AVar_lemma1: "\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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ lemma conforms_init_lvars: @@ -925,7 +925,7 @@ declare if_split [split] if_split_asm [split] option.split [split] option.split_asm [split] setup \map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\ -setup \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\ subsection "accessibility" diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/WellForm.thy Thu Jun 12 16:54:28 2025 +0200 @@ -2125,7 +2125,7 @@ qed declare split_paired_All [simp del] split_paired_Ex [simp del] -setup \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ lemma dynamic_mheadsD: @@ -2256,7 +2256,7 @@ qed declare split_paired_All [simp] split_paired_Ex [simp] setup \map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\ -setup \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\ (* Tactical version *) (* @@ -2399,7 +2399,7 @@ declare split_paired_All [simp del] split_paired_Ex [simp del] -setup \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ setup \map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\ lemma wt_is_type: "E,dt\v\T \ wf_prog (prg E) \ @@ -2425,7 +2425,7 @@ done declare split_paired_All [simp] split_paired_Ex [simp] setup \map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\ -setup \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\ lemma ty_expr_is_type: "\E\e\-T; wf_prog (prg E)\ \ is_type (prg E) T" diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Bali/WellType.thy Thu Jun 12 16:54:28 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 \map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\ inductive_cases wt_elim_cases [cases set]: "E,dt\In2 (LVar vn) \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 \map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))\ lemma is_acc_class_is_accessible: "is_acc_class G P C \ G\(Class C) accessible_in P" diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/HOL.thy Thu Jun 12 16:54:28 2025 +0200 @@ -13,7 +13,6 @@ abbrevs "?<" = "\\<^sub>\\<^sub>1" begin -ML_file \~~/src/Tools/simp_legacy.ML\ ML_file \~~/src/Tools/misc_legacy.ML\ ML_file \~~/src/Tools/try.ML\ ML_file \~~/src/Tools/quickcheck.ML\ diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Orderings.thy Thu Jun 12 16:54:28 2025 +0200 @@ -653,8 +653,8 @@ end setup \ - 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))) \ ML \ diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/SET_Protocol/Public_SET.thy --- a/src/HOL/SET_Protocol/Public_SET.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/SET_Protocol/Public_SET.thy Thu Jun 12 16:54:28 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])) \ diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Statespace/state_fun.ML Thu Jun 12 16:54:28 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 = diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/TLA/Action.thy Thu Jun 12 16:54:28 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])))); diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jun 12 16:54:28 2025 +0200 @@ -231,7 +231,7 @@ else K no_tac); \ -setup \map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver)\ +setup \map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_safe_solver fast_solver)\ ML \val temp_elim = make_elim oo temp_use\ diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Thu Jun 12 16:54:28 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 *) diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Jun 12 16:54:28 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, diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Tools/lin_arith.ML Thu Jun 12 16:54:28 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>\linarith_split\ (Scan.succeed (Thm.declaration_attribute add_split)) "declaration of split rules for arithmetic procedure" #> Method.setup \<^binding>\linarith\ diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Tools/simpdata.ML Thu Jun 12 16:54:28 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 diff -r 39a17ff4dd76 -r c0f166b39a3a src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/HOL/Transitive_Closure.thy Thu Jun 12 16:54:28 2025 +0200 @@ -1581,10 +1581,10 @@ setup \ 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)) \ lemma transp_rtranclp [simp]: "transp R\<^sup>*\<^sup>*" diff -r 39a17ff4dd76 -r c0f166b39a3a src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Thu Jun 12 10:38:02 2025 +0200 +++ b/src/Sequents/Sequents.thy Thu Jun 12 16:54:28 2025 +0200 @@ -10,8 +10,6 @@ keywords "print_pack" :: diag begin -ML_file \~~/src/Tools/simp_legacy.ML\ - setup Pure_Thy.old_appl_syntax_setup declare [[unify_trace_bound = 20, unify_search_bound = 40]] diff -r 39a17ff4dd76 -r c0f166b39a3a src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/Sequents/simpdata.ML Thu Jun 12 16:54:28 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 @@ -85,7 +85,8 @@ @{thms LK_extra_simps}; val LK_ss = - put_simpset LK_basic_ss \<^context> addsimps LK_simps + put_simpset LK_basic_ss \<^context> + |> Simplifier.add_simps LK_simps |> Simplifier.add_eqcong @{thm left_cong} |> Simplifier.add_cong @{thm imp_cong} |> simpset_of; diff -r 39a17ff4dd76 -r c0f166b39a3a src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/Tools/misc_legacy.ML Thu Jun 12 16:54:28 2025 +0200 @@ -3,6 +3,15 @@ Misc legacy stuff -- to be phased out eventually. *) +infix 4 addsimps delsimps addsimprocs delsimprocs; + +fun ctxt addsimps thms = ctxt |> Simplifier.add_simps thms; +fun ctxt delsimps thms = ctxt |> Simplifier.del_simps thms; + +fun ctxt addsimprocs procs = ctxt |> fold Simplifier.add_proc procs; +fun ctxt delsimprocs procs = ctxt |> fold Simplifier.del_proc procs; + + signature MISC_LEGACY = sig val add_term_names: term * string list -> string list diff -r 39a17ff4dd76 -r c0f166b39a3a src/Tools/simp_legacy.ML --- a/src/Tools/simp_legacy.ML Thu Jun 12 10:38:02 2025 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -(* Title: Tools/simp_legacy.ML - -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; - -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 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 diff -r 39a17ff4dd76 -r c0f166b39a3a src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/ZF/Tools/inductive_package.ML Thu Jun 12 16:54:28 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})); diff -r 39a17ff4dd76 -r c0f166b39a3a src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Thu Jun 12 10:38:02 2025 +0200 +++ b/src/ZF/Tools/typechk.ML Thu Jun 12 16:54:28 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 *)