Update documentation

- Mention --manual-lemma-induction
- Mention {:inductionTrigger}

docs/dev/news/5835.feat

@@ -11,6 +11,7 @@ More specifically:
    given variables.
 
    For an instance-member lemma, the variables may include the implicit `this` parameter.
+
    For an extreme lemma, the IH generated is the for corresponding prefix lemma, and the given variables may
    include the implicit parameter `_k`.
 
@@ -19,6 +20,7 @@ More specifically:
    an informational message is given.
 
 * If a lemma bears `{:induction}` or `{:induction true}`, then a list of induction variables is determined heuristically.
+
    If the list is empty, then a warning message is generated and no IH is generated. If the list is nonempty,
    an IH is generated and the list of variables is indicated in a tooltip.
 
@@ -30,12 +32,19 @@ More specifically:
 
 * If a lemma bears an `:induction` attribute other than those listed above, then an error is generated.
 
-* If a lemma bears no `:induction` attribute, then a list of induction variables is determined heuristically.
-   If this list is empty, then no IH is applied and no warning/info is given.
+* If a lemma bears no `:induction` attribute, and the `--manual-lemma-induction` flag is present, then no IH is generated.
+
+* Otherwise, a list of induction variables is determined heuristically.
+
+   If this list is empty, then no IH is generated and no warning/info is given.
 
    If the list is nonempty, then the machinery looks for matching patterns for the IH quantifier. If none are
-   found, then an informational message is generated, saying which candidate variables were used and saying that
-   no matching patterns were found.
+   found, then no IH is generated.  An informational message is generated, saying which candidate variables were
+   used and saying that no matching patterns were found.
+
+   If patterns are found, then an IH is generated, the list of variables and the patterns are indicated in tooltips,
+   and the patterns are used with the IH quantifier.
 
-   If patterns are found, then the list of variables and the patterns are indicated in tooltips, and the
-   patterns are used with the IH quantifier.
+   The pattern search can be overriden by providing patterns explicitly using the `{:inductionTrigger}` attribute.
+   This attribute has the same syntax as the `{:trigger}` attribute.  Using an empty list of triggers restores
+   Dafny's legacy behavior (no triggers for lemma induction hypotheses).