diff options
| -rw-r--r-- | doc/ProofGeneral.texi | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 6a0e0780..fd6bd65b 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -515,16 +515,17 @@ functions instead. -Now turn on active terminator minor mode by typing @kbd{C-c ;} and +Now turn on @dfn{active terminator minor mode} by typing @kbd{C-c ;} and enter: @lisp Module Walkthrough Import lib_logic; @end lisp -The command should be lit in pink (or inverse video if you don't have a -colour display). As LEGO imports each module, a line will appear in the -minibuffer showing the creation of context marks. Eventually the command -should turn blue, indicating that LEGO has successfully processed -it. Then type (on a separate line if you like): +Active terminator minor mode sends commands to the proof assistant as +you type them. The command should now be lit in pink (or inverse video +if you don't have a colour display). As LEGO imports each module, a +line will appear in the minibuffer showing the creation of context +marks. Eventually the command should turn blue, indicating that LEGO has +successfully processed it. Then type (on a separate line if you like): @lisp Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A); @end lisp |