From 0297fbeb04f2765f199cda661452f78ae6a8a967 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 3 Mar 2003 20:38:52 +0000
Subject: Note about M-x x-symbol-mode

---
 doc/ProofGeneral.texi | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index e0e5f568..97d16b72 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2129,6 +2129,17 @@ just use
 once it has been selected.  (Alternatively, customize the setting
 @code{@emph{PA}-x-symbol-enable}).
 
+You may also simply use @code{M-x x-symbol-mode} to turn on and off
+X-Symbol display in the scripting buffer, as you would when using
+X-Symbol for other modes, or indeed, as for any other Emacs minor mode.
+However, this way of turning on and off symbols will only affect the
+current script buffer, and will not change the status of any symbol
+configuration for the prover input/output (some proof assistants, such
+as Isabelle, have switches for enabling symbol output).  To make
+sure that symbol output is switched on or off for the prover
+as a whole, use the menu option mentioned above, or its underlying
+command, @code{M-x proof-x-symbol-toggle}.
+
 Notice that for proper symbol support, the proof assistant needs to have
 a special @i{token language}, or a special character set, to use
 symbols.  In this case, the proof assistant will output, and accept as
-- 
cgit v1.2.3