diff options
| author | Thomas Kleymann | 1998-10-22 18:53:14 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-10-22 18:53:14 +0000 |
| commit | da4900791d36269aaf4a9bcb4b8416a37811bdc0 (patch) | |
| tree | 55152413c6c4a0296e7acfcce18d177a803b5f1b | |
| parent | bed25bc850b8d6e50d56a9dd4b30e1fca2eb086a (diff) | |
minor change
| -rw-r--r-- | doc/ProofGeneral.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 0b97e197..68b74660 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -519,7 +519,7 @@ the goal. One needs to mark the proof of the theorem as an ACS. @item proof-atomic-sequents-list is a list of instructions for setting up ACSs. Each instruction is a list of the form @code{(@var{end} @var{start} &optional -@var{forget-command}}. @var{end} is a regular expression to recognise +@var{forget-command})}. @var{end} is a regular expression to recognise the last command in an ACS. @var{start} is a function. Its input is the last command of an ACS. Its output is a regular expression to recognise the first command of the ACS. It is evaluated once and the output is |