Update

1 files changed, 29 insertions, 19 deletions

diff --git a/FAQ b/FAQ
index 834d4edc..9942b990 100644
--- a/FAQ
+++ b/FAQ
@@ -1,9 +1,17 @@
-FAQs for Proof General
-======================
+FAQs for using Proof General
+============================
 
-$Id$
+For latest version, see http://www.proofgeneral.org/FAQ
+
+-----------------------------------------------------------------
 
-For latest version, see http://www.proofgeneral.org/ProofGeneral/FAQ
+Q. I'm using Proof General for prover X, then I load a file for prover Y.
+   The buffer doesn't enter the mode for prover Y.  Why not?
+
+A. Unfortunately the architecture of Proof General is designed so
+   that you can only use one prover at a time in the same Emacs
+   session.   If you want to run more than one prover at a time,
+   you have to run more than one Emacs.
 
 -----------------------------------------------------------------
 
@@ -55,17 +63,6 @@ A. Simply use the ordinary XEmacs menu: Options -> Save Options
 -----------------------------------------------------------------
 
 
-Q. I'm using Proof General for prover X, then I load a file for prover Y.
-   The buffer doesn't enter the mode for prover Y.  Why not?
-
-A. Unfortunately the architecture of Proof General is designed so
-   that you can only use one prover at a time in the same Emacs
-   session.   If you want to run more than one prover at a time,
-   you have to run more than one Emacs.
-
------------------------------------------------------------------
-
-
 Q. How do I use Proof General for Isabelle classic instead of Isabelle/Isar?
 
 A. There are several ways:
@@ -88,18 +85,31 @@ Q. When using X-Symbol, why do I sometimes see funny characters like
 A. These are part of the 8 bit character codes used by X Symbol to
    get symbols from particular fonts.  Sometimes X-Symbol forgets to
    fontify the buffer properly to make it use the right fonts.
-   To fix, type M-x x-font-lock-fontify-buffer or M-x x-symbol-fontify.
+   (That's being rather unkind to X-Symbol: several things can 
+    go wrong one way or another).
+
+   To fix, type M-x font-lock-fontify-buffer or M-x x-symbol-fontify.
    If that doesn't work, type M-x font-lock-mode twice to turn
    font-lock off then on.  Or reload the file.
    
    Note that X-Symbol is more robust when used with XEmacs/Mule.
 
    Read the X-Symbol documentation for (much) more information.
+   It's available at http://x-symbol.sourceforge.net/
 
 -----------------------------------------------------------------
 
 Q. Can I join any mailing lists for Proof General?
 
-A. Of course, email "majordomo@dcs.ed.ac.uk" with the 
-   lines "subscribe proofgeneral" or "subscribe proofgeneral-devel"
-   in the message body.
+A. Of course, email "proofgeneral-request@informatics.ed.ac.uk" 
+   with the line "subscribe" in the message body, to join the
+   user's and announcements list.
+
+   There is also a list for developers, proofgeneral-devel
+   Visit http://www.proofgeneral.org/mailinglist for more details.
+
+
+-----------------------------------------------------------------
+
+$Id$
+