From 689027e8088128c4b4fd887479ffcaecba507a88 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 18 Jul 2002 20:20:27 +0000
Subject: Mention how to enable X-Symbol.

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

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index bb775c7f..db9dbf70 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2042,6 +2042,13 @@ X-Symbol package and support has been provided in Proof General for a
 token language for your proof assistant.
 The X-Symbol package is available from
 @uref{http://x-symbol.sourceforge.net/}.
+To enable X-Symbol, use the menu item:
+@example
+  Proof-General -> Options -> X-Symbol
+@end example
+To enable it automatically every time you use Proof General,
+you need to customize the setting
+@code{@emph{PA}-x-symbol-enable}.
 
 Notice that for proper symbol support, the proof assistant needs to have
 a special @i{token language}, or a special character set, to use
-- 
cgit v1.2.3