| changeset 75033 | b55d84e41d61 |
| parent 75032 | 8d08bc7e8f98 |
| child 75034 | 890b70f96fe4 |
--- 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,6 +36,9 @@ 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]