diff -r d9bb81999d2c -r e1aa703c8cce src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Mar 25 13:52:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 25 13:52:23 2022 +0100
@@ -35,4 +35,7 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
+lemma "2 + 2 = 5"
+  sledgehammer[verbose, mepo, overlord]
+
 end