proper documentation for induction_rules Sledgehammer option
authordesharna
Mon, 20 Dec 2021 08:14:41 +0100
changeset 74957 089eeaaee525
parent 74956 a7183a0a33e1
child 74958 953f53f03437
proper documentation for induction_rules Sledgehammer option
src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Sun Dec 19 11:50:54 2021 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Dec 20 08:14:41 2021 +0100
@@ -947,7 +947,7 @@
 \item[\labelitemi] \textbf{\textit{exclude}:}
 Induction rules are ignored by the relevance filter.
 
-\item[\labelitemi] \textbf{\textit{instantiated}:}
+\item[\labelitemi] \textbf{\textit{instantiate}:}
 Induction rules are instantiated based on the conjecture and then
 considered by the relevance filter.