aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1998-11-25 14:49:56 +0000
committerDavid Aspinall1998-11-25 14:49:56 +0000
commit9471bab28345b532152c0f269a83b02bc3708510 (patch)
treec3ec75f47e522a481136b1d5a871907552da0143 /doc
parent570c90e025da1631a9dc8cff6bc9e64bff8467c2 (diff)
More polish.
Diffstat (limited to 'doc')
-rw-r--r--doc/ProofGeneral.texi8
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index b9695b28..a818b7d0 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -329,8 +329,8 @@ line:
into your @file{~/.emacs} file, where @var{proof-general-home} is the
top-level directory that was created when Proof General was unpacked.
-For more details on obtaining and installing Proof General,
-see @ref{Obtaining and Installing Proof General}.
+@xref{Obtaining and Installing Proof General} if you need more
+information.
@node Features of Proof General
@@ -366,8 +366,8 @@ be edited. Proof General has functions for @emph{asserting} or
regions.
For more details, see @ref{Basic Script Management},
-@xef{Script processing commands}.
-and @xref{Advanced Script Management}.
+@ref{Script processing commands}.
+and @ref{Advanced Script Management}.
@item @i{Script editing mode}@*
Proof General provides useful facilities for editing proof scripts,
including syntax hilighting and a menu to jump to particular goals,