# HG changeset patch
# User desharna
# Date 1743067828 -3600
# Node ID cc85ccb1a6b27c27fcd01e48ddef833da97fea2b
# Parent  a3f30dc0592059a424ac600bf7bc03b537a87c69
tuned signature

diff -r a3f30dc05920 -r cc85ccb1a6b2 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Mar 27 10:18:33 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Thu Mar 27 10:30:28 2025 +0100
@@ -11,6 +11,12 @@
   type xref = Facts.ref * Token.src list
   type tagged_xref = xref * modifier list
   type result = {name: string, command: string, time: Time.time, state: Proof.state}
+  type proof_method = Time.time option -> tagged_xref list -> Proof.state -> result option
+  type proof_method_options = {run_if_auto_try: bool}
+
+  val register_proof_method : string -> proof_method_options -> proof_method -> unit
+  val get_proof_method : string -> proof_method option
+
   val apply_proof_method : string -> Time.time option -> tagged_xref list ->
     Proof.state -> result option
   val try0 : Time.time option -> tagged_xref list -> Proof.state -> result list
@@ -89,14 +95,14 @@
       else
         ()
   in () end
-val _ = Symset.dest
 
-fun get_proof_method name = Symtab.lookup (Synchronized.value proof_methods) name;
+fun get_proof_method (name : string) : proof_method option =
+  Symtab.lookup (Synchronized.value proof_methods) name;
 
-fun get_all_proof_methods () =
+fun get_all_proof_methods () : (string * proof_method) list =
   Symtab.fold (fn x => fn xs => x :: xs) (Synchronized.value proof_methods) []
 
-fun get_all_proof_method_names () =
+fun get_all_proof_method_names () : string list =
   Symtab.fold (fn (name, _) => fn names => name :: names) (Synchronized.value proof_methods) []
 
 fun get_all_auto_try_proof_method_names () : string list =