| changeset 75340 | e1aa703c8cce |
| parent 75035 | ed510a3693e2 |
| child 75341 | 72cbbb4d98f3 |
--- 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