diff options
| author | David Aspinall | 1998-08-21 13:37:30 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-08-21 13:37:30 +0000 |
| commit | 922e663ce8a160d5f5b04fb0e2725a37548bcab0 (patch) | |
| tree | 3c8a273c6e4f6afa99d8c010e64404d96cdba4b6 | |
| parent | e133dc56af175b318551f9cc41d57630f5da4f93 (diff) | |
Typos and fixes in Walkthrough section.
| -rw-r--r-- | script-management.texinfo | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/script-management.texinfo b/script-management.texinfo index 6ca81ed7..a7232b3c 100644 --- a/script-management.texinfo +++ b/script-management.texinfo @@ -322,7 +322,7 @@ Here's a LEGO example of how script management is used. First, we turn on active terminator minor mode by typing @kbd{C-c ;} Then we enter -`Module Walthrough Import lib_logic;' +`Module Walkthrough Import lib_logic;' 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 @@ -330,7 +330,7 @@ response buffer 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) -@samp{Goal bland_commutes: @{A,b:Prop@} and A B -> and B A;} +@samp{Goal bland_commutes: @{A,B:Prop@} (and A B) -> (and B A);} The goal should be echoed in the response buffer. |