changeset 82397 | ae2af2e085fd |
parent 82396 | 7230281bde03 |
child 82455 | eaf0b4673ab2 |
--- a/src/HOL/Tools/try0.ML Wed Apr 02 11:18:35 2025 +0200 +++ b/src/HOL/Tools/try0.ML Fri Apr 04 15:27:28 2025 +0200 @@ -107,7 +107,7 @@ fun get_proof_method_or_noop name = (case get_proof_method name of - NONE => noop_proof_method + NONE => (warning ("Proof method \"" ^ name ^ "\" is undefined"); noop_proof_method) | SOME proof_method => proof_method) fun maybe_apply_proof_method name mode : proof_method =