| changeset 75341 | 72cbbb4d98f3 |
| parent 75340 | e1aa703c8cce |
| child 77602 | 7c25451ae2c1 |
--- 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,7 +35,4 @@ 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