diff options
| author | David Aspinall | 1999-09-13 14:31:42 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-09-13 14:31:42 +0000 |
| commit | 397ba54871820625bc4f9d0a5098506bad99ffac (patch) | |
| tree | b88e40304d0f9d82636c62937e8589cc084da989 | |
| parent | 6ed9e5bdfc5840188a33a7f077331b4d5ec8d510 (diff) | |
Emphasised that user can still use the shell
| -rw-r--r-- | doc/ProofGeneral.texi | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index a46f1302..07f5d815 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -427,8 +427,10 @@ Communication takes place via two or three buffers. The @dfn{script buffer} holds input, the commands to construct a proof. The @dfn{goals buffer} displays the current list of subgoals to be solved. The @dfn{response buffer} displays other output from the proof assistant. -This means that the user only sees the output from the most recent proof +This means that the user normally only sees the output from the most recent proof step, rather than a screen full of output from the proof assistant. +However, the user can still access the proof assistant shell to examine +it and run commands. @c Optionally, the goals buffer and script buffer can be identified. For more details, see @ref{Basic Script Management}, @ref{Script |