@@ -80,9 +80,8 @@ Then, issue the ``:elab <hole>`` command at the REPL
80to enter the elaboration shell.
80to enter the elaboration shell.
82At the shell, you can enter proof tactics to alter the proof state.
82At the shell, you can enter proof tactics to alter the proof state.
83+You can view the system-provided tactics prior to entering the shell
83−It is recommended to issue ``:module Language.Reflection.Elab``
84+by issuing the REPL command ``:browse Language.Reflection.Elab.Tactics``.
84−prior to entering the elaboration shell in order to have the system-provided
85−tactics available to you.
86When you have discharged all goals, you can complete the proof
85When you have discharged all goals, you can complete the proof
87using the ``:qed`` command and receive in return an elaboration script
86using the ``:qed`` command and receive in return an elaboration script
88that fills the hole.
87that fills the hole.