--- a/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 11:27:21 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 12:57:22 2021 +0200
@@ -1000,7 +1000,7 @@
\item[\labelitemi] \textbf{\textit{keep\_lams}:}
Keep the $\lambda$-abstractions in the generated problems. This is available
-only with provers that support the TH0 syntax.
+only with provers that support $\lambda$s.
\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used
depends on the ATP and should be the most efficient scheme for that ATP.