@@ -81,8 +81,7 @@ to enter the elaboration shell.
82The interactive elaboration shell accepts the following commands:
82The interactive elaboration shell accepts the following commands:
84−- ``:abandon``, or ``:q`` for short,
84+- ``:abandon`` gives up on proving the current lemma and quits the elaboration shell.
85− quits the elaboration shell, which abandons proving the current lemma.
87- ``:state`` displays the current state of the term being constructed.
86- ``:state`` displays the current state of the term being constructed.