diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 23aba63b..c2cb3be5 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -924,18 +924,15 @@ example in Isabelle with semi-colons, but these will not appear in the final text. Coq, on the other hand, requires a full-stop terminator at the end of -each line, so @kbd{C-c .} is the key binding used to turn on -electric terminator. If you don't know what the terminator character -is, you can find the option anyway on the menu: +each line. If you want to enable electric terminator, use the menu item: @code{Proof-General -> Quick Options -> Processing -> Electric Terminator} -which also shows the key binding. -If you want to use electric terminator, you can customize Proof -General to enable it every time if you want, @xref{Customizing Proof -General}. For the common options, customization is easy: just -use the menu item @code{Proof General -> Quick Options} to make your choices, -and @code{Proof-General -> Quick Options -> Save Options} to -save your choices. +If you want to keep electric terminator enabled all the time, you can +customize Proof General to do so, @xref{Customizing Proof General}. For +the common options, customization is easy: just use the menu item +@code{Proof General -> Quick Options} to make your choices, and +@code{Proof-General -> Quick Options -> Save Options} to save your +choices. @@ -4342,7 +4339,7 @@ The same for a ``Print '' query. @item C-c C-a C-b The same for a ``About '' query. @item C-c C-a C-a -The same for a ``SearchAbout '' query (no C-u prefix). +The same for a ``Search '' query (no C-u prefix). @item C-c C-a C-o The same for a Search ``SearchIsos'' (no C-u prefix). |