src/HOL/Sledgehammer.thy

--- a/src/HOL/Sledgehammer.thy	Wed Mar 15 13:01:57 2023 +0100
+++ b/src/HOL/Sledgehammer.thy	Wed Mar 15 15:28:44 2023 +0100
@@ -35,10 +35,4 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
-(*
-lemma "x - y + y = (x::nat)"
-  sledgehammer[e, abduce = 10]
-  oops
-*)
-
 end