diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 110e3253e..051c28f91 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -893,18 +893,15 @@ quantification or an implication. This clears the hypothesis :n:`@ident` and all the hypotheses that depend on it. -.. tacv:: clearbody @ident +.. tacv:: clearbody {+ @ident} :name: clearbody - This tactic expects :n:`@ident` to be a local definition then clears its - body. Otherwise said, this tactic turns a definition into an assumption. + This tactic expects :n:`{+ @ident}` to be local definitions and clears their + respective bodies. + In other words, it turns the given definitions into assumptions. .. exn:: @ident is not a local definition. -.. tacv:: clearbody {+ @ident} - - This is equivalent to :n:`clearbody @ident. ... clearbody @ident.` - .. tacn:: revert {+ @ident} :name: revert |