--- 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
@@ -37,7 +37,7 @@
(*
lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
- sledgehammer [slices = 4]
+ sledgehammer [max_proofs = 3]
oops
*)