author | nipkow |
Thu, 16 Mar 2023 13:37:49 +0100 | |
changeset 77672 | 34176328fc67 |
parent 77670 | b9e9b818d7b0 (diff) |
parent 77671 | 8a6a79ed5a83 (current diff) |
child 77682 | a76f49a03448 |
--- a/src/HOL/Sledgehammer.thy Thu Mar 16 08:30:00 2023 +0100 +++ b/src/HOL/Sledgehammer.thy Thu Mar 16 13:37:49 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