--- a/src/Doc/Isar_Ref/Generic.thy Wed May 21 20:13:43 2025 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Wed May 21 20:13:43 2025 +0200
@@ -1038,12 +1038,11 @@
text \<open>
\begin{mldecls}
- @{define_ML_infix setloop: "Proof.context *
- (Proof.context -> int -> tactic) -> Proof.context"} \\
- @{define_ML_infix addloop: "Proof.context *
- (string * (Proof.context -> int -> tactic))
- -> Proof.context"} \\
- @{define_ML_infix delloop: "Proof.context * string -> Proof.context"} \\
+ @{define_ML Simplifier.set_loop: "(Proof.context -> int -> tactic) ->
+ Proof.context -> Proof.context"} \\
+ @{define_ML Simplifier.add_loop: "string * (Proof.context -> int -> tactic) ->
+ Proof.context -> Proof.context"} \\
+ @{define_ML Simplifier.del_loop: "string -> Proof.context -> Proof.context"} \\
@{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
@{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
@{define_ML Splitter.add_split_bang: "
@@ -1060,14 +1059,14 @@
Another possibility is to apply an elimination rule on the assumptions. More
adventurous loopers could start an induction.
- \<^descr> \<open>ctxt setloop tac\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
+ \<^descr> \<^ML>\<open>Simplifier.set_loop\<close>~\<open>tac ctxt\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
- \<^descr> \<open>ctxt addloop (name, tac)\<close> adds \<open>tac\<close> as an additional looper tactic
+ \<^descr> \<^ML>\<open>Simplifier.add_loop\<close>~\<open>(name, tac) ctxt\<close> adds \<open>tac\<close> as an additional looper tactic
with name \<open>name\<close>, which is significant for managing the collection of
loopers. The tactic will be tried after the looper tactics that had
already been present in \<open>ctxt\<close>.
- \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was associated with
+ \<^descr> \<^ML>\<open>Simplifier.del_loop\<close>~\<open>name ctxt\<close> deletes the looper tactic that was associated with
\<open>name\<close> from \<open>ctxt\<close>.
\<^descr> \<^ML>\<open>Splitter.add_split\<close>~\<open>thm ctxt\<close> adds split tactic
--- a/src/Pure/raw_simplifier.ML Wed May 21 20:13:43 2025 +0200
+++ b/src/Pure/raw_simplifier.ML Wed May 21 20:13:43 2025 +0200
@@ -102,10 +102,13 @@
val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
val prems_of: Proof.context -> thm list
val add_prems: thm list -> Proof.context -> Proof.context
+ val loop_tac: Proof.context -> int -> tactic
+ val set_loop: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
+ val add_loop: string * (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
+ val del_loop: string -> Proof.context -> Proof.context
val solvers: Proof.context -> solver list * solver list
val solver: Proof.context -> solver -> int -> tactic
val set_solvers: solver list -> Proof.context -> Proof.context
- val loop_tac: Proof.context -> int -> tactic
val default_mk_sym: Proof.context -> thm -> thm option
val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
Proof.context -> Proof.context
@@ -868,22 +871,28 @@
map_simpset2 (fn (congs, procs, mk_rews, term_ord, _, loop_tacs, solvers) =>
(congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
-fun ctxt setloop tac = ctxt |>
+fun set_loop tac =
map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
(congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
-fun ctxt addloop (name, tac) = ctxt |>
+fun ctxt setloop tac = ctxt |> set_loop tac;
+
+fun add_loop (name, tac) =
map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
(congs, procs, mk_rews, term_ord, subgoal_tac,
AList.update (op =) (name, tac) loop_tacs, solvers));
-fun ctxt delloop name = ctxt |>
+fun ctxt addloop tac = ctxt |> add_loop tac;
+
+fun del_loop name ctxt = ctxt |>
map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
(congs, procs, mk_rews, term_ord, subgoal_tac,
(if AList.defined (op =) loop_tacs name then ()
else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name);
AList.delete (op =) name loop_tacs), solvers));
+fun ctxt delloop name = ctxt |> del_loop name;
+
fun ctxt setSSolver solver = ctxt |> map_simpset2
(fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
(congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));