| changeset 82363 | 3a7fc54b50ca |
| parent 82362 | 396676efbd6d |
| child 82364 | 5af097d05e99 |
--- a/src/HOL/Tools/try0.ML Thu Mar 27 13:44:42 2025 +0100 +++ b/src/HOL/Tools/try0.ML Thu Mar 27 14:33:08 2025 +0100 @@ -17,6 +17,7 @@ val register_proof_method : string -> proof_method_options -> proof_method -> unit val get_proof_method : string -> proof_method option + val get_all_proof_method_names : unit -> string list datatype mode = Auto_Try | Try | Normal val generic_try0 : mode -> Time.time option -> tagged_xref list -> Proof.state ->