| changeset 75034 | 890b70f96fe4 |
| parent 75033 | b55d84e41d61 |
| child 75035 | ed510a3693e2 |
--- a/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100 @@ -36,9 +36,6 @@ ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close> (* -lemma "1 + 1 = 3" - sledgehammer[verbose] - lemma "1 + 1 = 2" sledgehammer [slices = 40, max_proofs = 40]