--- a/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Tue Aug 13 19:28:58 2024 +0200
+++ b/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Tue Aug 13 21:09:51 2024 +0200
@@ -356,12 +356,12 @@
lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.upd_simproc]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc Record.upd_simproc) 1\<close>)
done
lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -372,7 +372,7 @@
lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -383,7 +383,7 @@
lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply auto
done
@@ -417,7 +417,7 @@
lemma "\<exists>r. A155 r = x"
apply (tactic \<open>simp_tac
- (put_simpset HOL_basic_ss \<^context> addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
+ (put_simpset HOL_basic_ss \<^context> |> Simplifier.add_proc (Record.ex_sel_eq_simproc)) 1\<close>)
done
print_record many_A
--- a/src/HOL/Decision_Procs/cooper_tac.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Tue Aug 13 21:09:51 2024 +0200
@@ -53,7 +53,8 @@
div_by_1 mod_by_1 div_by_Suc_0 mod_by_Suc_0
Suc_eq_plus1}
addsimps @{thms ac_simps}
- addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>]
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
val simpset0 =
put_simpset HOL_basic_ss ctxt
addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1 simp_thms}
--- a/src/HOL/Decision_Procs/langford.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Tue Aug 13 21:09:51 2024 +0200
@@ -176,7 +176,7 @@
let
val ctxt' =
Context_Position.set_visible false (put_simpset dlo_ss ctxt)
- addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
+ addsimps @{thms dnf_simps} |> Simplifier.add_proc reduce_ex_simproc
val dnfex_conv = Simplifier.rewrite ctxt'
val pcv =
Simplifier.rewrite
--- a/src/HOL/Decision_Procs/mir_tac.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Aug 13 21:09:51 2024 +0200
@@ -68,14 +68,16 @@
(* Transform the term*)
val (t,np,nh) = prepare_for_mir q g
(* Some simpsets for dealing with mod div abs and nat*)
- val mod_div_simpset = put_simpset HOL_basic_ss ctxt
- addsimps [refl, @{thm mod_add_eq},
- @{thm mod_self},
- @{thm div_0}, @{thm mod_0},
- @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
- @{thm "Suc_eq_plus1"}]
- addsimps @{thms add.assoc add.commute add.left_commute}
- addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>]
+ val mod_div_simpset =
+ put_simpset HOL_basic_ss ctxt
+ addsimps [refl, @{thm mod_add_eq},
+ @{thm mod_self},
+ @{thm div_0}, @{thm mod_0},
+ @{thm div_by_1}, @{thm mod_by_1}, @{thm div_by_Suc_0}, @{thm mod_by_Suc_0},
+ @{thm "Suc_eq_plus1"}]
+ addsimps @{thms add.assoc add.commute add.left_commute}
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_nat\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>cancel_div_mod_int\<close>
val simpset0 = put_simpset HOL_basic_ss ctxt
addsimps @{thms minus_div_mult_eq_mod [symmetric] Suc_eq_plus1}
addsimps comp_ths
--- a/src/HOL/Examples/Records.thy Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Examples/Records.thy Tue Aug 13 21:09:51 2024 +0200
@@ -244,7 +244,7 @@
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
- addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -255,7 +255,7 @@
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
- addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply simp
done
@@ -266,7 +266,7 @@
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
apply (tactic \<open>simp_tac (put_simpset HOL_basic_ss \<^context>
- addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
+ |> Simplifier.add_proc (Record.split_simproc (K ~1))) 1\<close>)
apply auto
done
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Aug 13 21:09:51 2024 +0200
@@ -35,7 +35,7 @@
val beta_ss =
simpset_of (put_simpset HOL_basic_ss \<^context>
- addsimps @{thms simp_thms} addsimprocs [\<^simproc>\<open>beta_cfun_proc\<close>])
+ addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\<open>beta_cfun_proc\<close>)
fun is_cpo thy T = Sign.of_sort thy (T, \<^sort>\<open>cpo\<close>)
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Aug 13 21:09:51 2024 +0200
@@ -108,7 +108,7 @@
val beta_ss =
simpset_of (put_simpset HOL_basic_ss \<^context>
- addsimps @{thms simp_thms} addsimprocs [\<^simproc>\<open>beta_cfun_proc\<close>])
+ addsimps @{thms simp_thms} |> Simplifier.add_proc \<^simproc>\<open>beta_cfun_proc\<close>)
(******************************************************************************)
(******************************** theory data *********************************)
--- a/src/HOL/Hoare/hoare_tac.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Tue Aug 13 21:09:51 2024 +0200
@@ -157,7 +157,7 @@
fun basic_simp_tac ctxt var_names tac =
simp_tac
(put_simpset HOL_basic_ss ctxt
- addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
+ addsimps [mem_Collect_eq, @{thm split_conv}] |> Simplifier.add_proc Record.simproc)
THEN_MAYBE' max_simp_tac ctxt var_names tac;
--- a/src/HOL/Library/Cancellation/cancel.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Library/Cancellation/cancel.ML Tue Aug 13 21:09:51 2024 +0200
@@ -48,9 +48,10 @@
let
val t = Thm.term_of ct
val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt
- val pre_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
- Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close> addsimprocs
- [\<^simproc>\<open>NO_MATCH\<close>]) (Thm.cterm_of ctxt t');
+ val pre_simplified_ct =
+ Simplifier.full_rewrite (clear_simpset ctxt
+ addsimps Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_pre\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (Thm.cterm_of ctxt t');
val t' = Thm.term_of (Thm.rhs_of pre_simplified_ct)
val export = singleton (Variable.export ctxt' ctxt)
@@ -66,11 +67,11 @@
val canceled_thm = Cancel_Numerals_Fun.proc ctxt (Thm.rhs_of pre_simplified_ct)
fun add_pre_simplification thm = @{thm Pure.transitive} OF [pre_simplified_ct, thm]
fun add_post_simplification thm =
- (let val post_simplified_ct = Simplifier.full_rewrite (clear_simpset ctxt addsimps
- Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_post\<close> addsimprocs
- [\<^simproc>\<open>NO_MATCH\<close>])
- (Thm.rhs_of thm)
- in @{thm Pure.transitive} OF [thm, post_simplified_ct] end)
+ let val post_simplified_ct =
+ Simplifier.full_rewrite (clear_simpset ctxt
+ addsimps Named_Theorems.get ctxt \<^named_theorems>\<open>cancelation_simproc_post\<close>
+ |> Simplifier.add_proc \<^simproc>\<open>NO_MATCH\<close>) (Thm.rhs_of thm)
+ in @{thm Pure.transitive} OF [thm, post_simplified_ct] end
in
Option.map (export o add_post_simplification o add_pre_simplification) canceled_thm
end
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Aug 13 21:09:51 2024 +0200
@@ -1380,8 +1380,10 @@
simp_tac ind_ss1' i
| _ $ (Const (\<^const_name>\<open>Not\<close>, _) $ _) =>
resolve_tac context2 freshs2' i
- | _ => asm_simp_tac (put_simpset HOL_basic_ss context3 addsimps
- pt2_atoms addsimprocs [perm_simproc]) i)) 1])
+ | _ =>
+ asm_simp_tac (put_simpset HOL_basic_ss context3
+ addsimps pt2_atoms
+ |> Simplifier.add_proc perm_simproc) i)) 1])
val final = Proof_Context.export context3 context2 [th]
in
resolve_tac context2 final 1
@@ -1560,7 +1562,7 @@
resolve_tac ctxt [rec_induct] 1 THEN REPEAT
(simp_tac (put_simpset HOL_basic_ss ctxt
addsimps flat perm_simps'
- addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1 THEN
(resolve_tac ctxt rec_intrs THEN_ALL_NEW
asm_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_bij @ perm_bij))) 1))))
val ths' = map (fn ((P, Q), th) =>
@@ -1972,8 +1974,8 @@
(fn {context = ctxt, ...} => EVERY
[cut_facts_tac [th'] 1,
full_simp_tac (put_simpset HOL_ss ctxt
- addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
- addsimprocs [NominalPermeq.perm_app_simproc]) 1,
+ addsimps (rec_eqns @ pi1_pi2_eqs @ perm_swap)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1,
full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @
fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
end;
@@ -2005,8 +2007,8 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs')))
(fn _ => simp_tac (put_simpset HOL_ss context''
- addsimps pi1_pi2_eqs @ rec_eqns
- addsimprocs [NominalPermeq.perm_app_simproc]) 1 THEN
+ addsimps (pi1_pi2_eqs @ rec_eqns)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc) 1 THEN
TRY (simp_tac (put_simpset HOL_ss context'' addsimps
(fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
--- a/src/HOL/Nominal/nominal_inductive.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Aug 13 21:09:51 2024 +0200
@@ -280,8 +280,9 @@
fun eqvt_ss ctxt =
put_simpset HOL_basic_ss ctxt
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
- NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ |> Simplifier.add_proc (mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>])
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
val perm_bij = Global_Theory.get_thms thy "perm_bij";
val fs_atoms = map (fn aT => Global_Theory.get_thm thy
@@ -352,8 +353,9 @@
map (fold_rev (NominalDatatype.mk_perm [])
(rev pis' @ pis)) params' @ [z]))) ihyp;
fun mk_pi th =
- Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
- addsimprocs [NominalDatatype.perm_simproc])
+ Simplifier.simplify (put_simpset HOL_basic_ss ctxt'
+ addsimps [@{thm id_apply}]
+ |> Simplifier.add_proc NominalDatatype.perm_simproc)
(Simplifier.simplify (eqvt_ss ctxt')
(fold_rev (mk_perm_bool ctxt' o Thm.cterm_of ctxt')
(rev pis' @ pis) th));
@@ -399,7 +401,7 @@
REPEAT_DETERM_N (length gprems)
(simp_tac (put_simpset HOL_basic_ss goal_ctxt4
addsimps [inductive_forall_def']
- addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
+ |> Simplifier.add_proc NominalDatatype.perm_simproc) 1 THEN
resolve_tac goal_ctxt4 gprems2 1)]));
val final = Goal.prove ctxt' [] [] (Thm.term_of concl)
(fn {context = goal_ctxt5, ...} =>
@@ -468,8 +470,9 @@
fun cases_eqvt_simpset ctxt =
put_simpset HOL_ss ctxt
- addsimps eqvt_thms @ swap_simps @ perm_pi_simp
- addsimprocs [NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ addsimps (eqvt_thms @ swap_simps @ perm_pi_simp)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
fun simp_fresh_atm ctxt =
Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps fresh_atm);
@@ -625,10 +628,12 @@
val (([t], [pi]), ctxt1) = lthy |>
Variable.import_terms false [Thm.concl_of raw_induct] ||>>
Variable.variant_fixes ["pi"];
- fun eqvt_simpset ctxt = put_simpset HOL_basic_ss ctxt addsimps
- (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
- [mk_perm_bool_simproc names,
- NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ fun eqvt_simpset ctxt =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp)
+ |> Simplifier.add_proc (mk_perm_bool_simproc names)
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
val ps = map (fst o HOLogic.dest_imp)
(HOLogic.dest_conj (HOLogic.dest_Trueprop t));
fun eqvt_tac ctxt pi (intr, vs) st =
--- a/src/HOL/Nominal/nominal_inductive2.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue Aug 13 21:09:51 2024 +0200
@@ -299,8 +299,9 @@
fun eqvt_ss ctxt =
put_simpset HOL_basic_ss ctxt
addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
- addsimprocs [mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>],
- NominalPermeq.perm_app_simproc, NominalPermeq.perm_fun_simproc];
+ |> Simplifier.add_proc (mk_perm_bool_simproc [\<^const_name>\<open>Fun.id\<close>])
+ |> Simplifier.add_proc NominalPermeq.perm_app_simproc
+ |> Simplifier.add_proc NominalPermeq.perm_fun_simproc;
val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
@@ -412,7 +413,7 @@
fun mk_pi th =
Simplifier.simplify
(put_simpset HOL_basic_ss ctxt'' addsimps [@{thm id_apply}]
- addsimprocs [NominalDatatype.perm_simproc])
+ |> Simplifier.add_proc NominalDatatype.perm_simproc)
(Simplifier.simplify (eqvt_ss ctxt'')
(fold_rev (mk_perm_bool ctxt'' o Thm.cterm_of ctxt'')
(pis' @ pis) th));
@@ -435,7 +436,7 @@
[REPEAT_DETERM_N (length gprems)
(simp_tac (put_simpset HOL_basic_ss goal_ctxt4
addsimps [inductive_forall_def']
- addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
+ |> Simplifier.add_proc NominalDatatype.perm_simproc) 1 THEN
resolve_tac goal_ctxt4 gprems2 1)]));
val final = Goal.prove ctxt'' [] [] (Thm.term_of concl)
(fn {context = goal_ctxt5, ...} =>
--- a/src/HOL/Nominal/nominal_permeq.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Tue Aug 13 21:09:51 2024 +0200
@@ -142,7 +142,8 @@
let
val ctxt' = ctxt
addsimps (maps (Proof_Context.get_thms ctxt) dyn_thms @ eqvt_thms)
- addsimprocs [perm_fun_simproc, perm_app_simproc]
+ |> Simplifier.add_proc perm_fun_simproc
+ |> Simplifier.add_proc perm_app_simproc
|> fold Simplifier.del_cong weak_congs
|> fold Simplifier.add_cong strong_congs
in
@@ -219,7 +220,7 @@
("analysing permutation compositions on the lhs",
fn st => EVERY
[resolve_tac ctxt [trans] i,
- asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i,
+ asm_full_simp_tac (empty_simpset ctxt |> Simplifier.add_proc perm_compose_simproc) i,
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st);
fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
--- a/src/HOL/Statespace/state_fun.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Statespace/state_fun.ML Tue Aug 13 21:09:51 2024 +0200
@@ -80,18 +80,18 @@
simp_tac (put_simpset HOL_basic_ss ctxt
addsimps @{thms list.inject list.distinct char.inject
cong_exp_iff_simps simp_thms}
- addsimprocs [lazy_conj_simproc]
+ |> Simplifier.add_proc lazy_conj_simproc
|> Simplifier.add_cong @{thm block_conj_cong});
end;
val lookup_ss =
- simpset_of (put_simpset HOL_basic_ss \<^context>
+ simpset_of ((put_simpset HOL_basic_ss \<^context>
addsimps (@{thms list.inject} @ @{thms char.inject}
@ @{thms list.distinct} @ @{thms simp_thms}
@ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
@{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
- addsimprocs [lazy_conj_simproc]
+ |> Simplifier.add_proc lazy_conj_simproc)
addSolver StateSpace.distinctNameSolver
|> fold Simplifier.add_cong @{thms block_conj_cong});
@@ -173,7 +173,8 @@
simpset_of (put_simpset HOL_ss \<^context> addsimps
(@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
@ @{thms list.distinct})
- addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
+ |> Simplifier.add_proc lazy_conj_simproc
+ |> Simplifier.add_proc StateSpace.distinct_simproc
|> fold Simplifier.add_cong @{thms block_conj_cong});
in
@@ -395,7 +396,7 @@
(simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss));
val activate_simprocs =
if simprocs_active then I
- else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]);
+ else Simplifier.map_ss (fold Simplifier.add_proc [lookup_simproc, update_simproc]);
in
context
|> activate_simprocs
--- a/src/HOL/Statespace/state_space.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Statespace/state_space.ML Tue Aug 13 21:09:51 2024 +0200
@@ -338,7 +338,7 @@
val tt' = tt |> fold upd all_names;
val context' =
Context_Position.set_visible false ctxt
- addsimprocs [distinct_simproc]
+ |> Simplifier.add_proc distinct_simproc
|> Context_Position.restore_visible ctxt
|> Context.Proof
|> map_declinfo (K declinfo)
--- a/src/HOL/Tools/record.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Tools/record.ML Tue Aug 13 21:09:51 2024 +0200
@@ -1442,11 +1442,11 @@
else NONE
end));
- val simprocs = if has_rec goal then [split_simproc P] else [];
+ val add_simproc = if has_rec goal then Simplifier.add_proc (split_simproc P) else I;
val thms' = @{thms o_apply K_record_comp} @ thms;
in
EVERY split_frees_tacs THEN
- full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' addsimprocs simprocs) i
+ full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' |> add_simproc) i
end);
--- a/src/Tools/induct.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/Tools/induct.ML Tue Aug 13 21:09:51 2024 +0200
@@ -229,8 +229,8 @@
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)),
- simpset_of (empty_simpset \<^context>
- addsimprocs [rearrange_eqs_simproc] addsimps [Drule.norm_hhf_eq]));
+ simpset_of ((empty_simpset \<^context>
+ |> Simplifier.add_proc rearrange_eqs_simproc) addsimps [Drule.norm_hhf_eq]));
fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1), simpset1),
((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2), simpset2)) =
((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),