# HG changeset patch
# User desharna
# Date 1639984481 -3600
# Node ID 089eeaaee525430f356eebeaad4115b59713e3af
# Parent  a7183a0a33e1fb7f4f4699f68cf20c6a090f2117
proper documentation for induction_rules Sledgehammer option

diff -r a7183a0a33e1 -r 089eeaaee525 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.