Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Isar_Ref/Generic.thy
changeset 82651 d374a7eb121a
parent 82650 e153ab596247 
--- 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
@@ -955,10 +955,14 @@
   @{define_ML_type solver} \\
   @{define_ML Simplifier.mk_solver: "string ->
   (Proof.context -> int -> tactic) -> solver"} \\
-  @{define_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\
-  @{define_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\
+  @{define_ML Simplifier.set_safe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_safe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.set_unsafe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_unsafe_solver: "
+  solver -> Proof.context -> Proof.context"} \\
   \end{mldecls}
 
   A solver is a tactic that attempts to solve a subgoal after simplification.
@@ -989,14 +993,14 @@
   \<^descr> \<^ML>\<open>Simplifier.mk_solver\<close>~\<open>name tac\<close> turns \<open>tac\<close> into a solver; the
   \<open>name\<close> is only attached as a comment and has no further significance.
 
-  \<^descr> \<open>ctxt setSSolver solver\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
+  \<^descr> \<^ML>\<open>Simplifier.set_safe_solver\<close>~\<open>solver ctxt\<close> installs \<open>solver\<close> as the safe solver of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addSSolver solver\<close> adds \<open>solver\<close> as an additional safe solver; it
+  \<^descr> \<^ML>\<open>Simplifier.add_safe_solver\<close>~\<open>solver ctxt\<close> adds \<open>solver\<close> as an additional safe solver; it
   will be tried after the solvers which had already been present in \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt setSolver solver\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
+  \<^descr> \<^ML>\<open>Simplifier.set_unsafe_solver\<close>~\<open>solver ctxt\<close> installs \<open>solver\<close> as the unsafe solver of \<open>ctxt\<close>.
 
-  \<^descr> \<open>ctxt addSolver solver\<close> adds \<open>solver\<close> as an additional unsafe solver; it
+  \<^descr> \<^ML>\<open>Simplifier.add_unsafe_solver\<close>~\<open>solver ctxt\<close> adds \<open>solver\<close> as an additional unsafe solver; it
   will be tried after the solvers which had already been present in \<open>ctxt\<close>.
isabelle