diff options
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index d1a70b5619..e9aacba3a5 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -358,8 +358,10 @@ same bullet ``b``. See the example below. Different bullets can be used to nest levels. The scope of bullet does not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further -nesting levels provided they are delimited by these. Available bullets -are ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period). +nesting levels provided they are delimited by these. Bullets are made of +repeated ``-``, ``+`` or ``*`` symbols: + +.. prodn:: bullet ::= {+ - } %| {+ + } %| {+ * } Note again that when a focused goal is proved a message is displayed together with a suggestion about the right bullet or ``}`` to unfocus it |