diff options
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 3d902a9c76..f286533d78 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -109,7 +109,7 @@ Rewriting with Leibniz and setoid equality For each selected hypothesis and/or the conclusion, :tacn:`rewrite` finds the first matching subterm in - depth-first search order. Only subterms identical to the + depth-first search order. Only subterms identical to that first matched subterm are rewritten. If the `at` clause is specified, only these subterms are considered when counting occurrences. To select a different set of matching subterms, you can |