diff options
| author | Jim Fehrle | 2021-01-28 13:20:07 -0800 |
|---|---|---|
| committer | GitHub | 2021-01-28 13:20:07 -0800 |
| commit | de7f7fe34828debfa4bd5130810ee5ccc0ea0170 (patch) | |
| tree | 83304e229bb42f46ed35f164c6864986170849ee | |
| parent | ae7b304a5a24816d31fbcef1212e15b98bada7a1 (diff) | |
Update doc/sphinx/proofs/writing-proofs/rewriting.rst
| -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 |