diff -r 8d08bc7e8f98 -r b55d84e41d61 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy	Mon Jan 31 16:09:23 2022 +0100
@@ -36,6 +36,9 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
 (*
+lemma "1 + 1 = 3"
+  sledgehammer[verbose]
+
 lemma "1 + 1 = 2"
   sledgehammer [slices = 40, max_proofs = 40]