author | blanchet |
Wed, 15 Mar 2023 15:28:44 +0100 | |
changeset 77670 | b9e9b818d7b0 |
parent 77669 | 8f96ac621bfd |
child 77672 | 34176328fc67 |
child 77673 | 08fcde7c55c0 |
child 77684 | 71f001027a13 |
--- 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