--- a/src/Doc/Sledgehammer/document/root.tex Wed Aug 17 15:09:53 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Aug 17 18:20:10 2022 +0200
@@ -1129,9 +1129,9 @@
\opsmart{isar\_proofs}{no\_isar\_proofs}
Specifies whether Isar proofs should be output in addition to one-line proofs.
The construction of Isar proof is still experimental and may sometimes fail;
-however, when they succeed they are usually faster and more intelligible than
-one-line proofs. If the option is set to \textit{smart} (the default), Isar
-proofs are only generated when no working one-line proof is available.
+however, when they succeed they can be faster and sometimes more intelligible
+than one-line proofs. If the option is set to \textit{smart} (the default), Isar
+proofs are generated only when no working one-line proof is available.
\opdefault{compress}{int}{smart}
Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}