From 0005f77be3219f1b7b00fd81d9485a207c6f17a1 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 May 2001 17:55:26 +0000
Subject: AF2 -> PhoX name change

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

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 96ee46dd..9766b174 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -164,7 +164,7 @@ generic Emacs interface for proof assistants.
 
 Proof General @value{version} has been tested with XEmacs
 @value{xemacsversion} and FSF GNU Emacs @value{fsfversion}.  It is
-supplied ready customized for the proof assistants AF2, Coq, Lego, 
+supplied ready customized for the proof assistants PhoX, Coq, Lego, 
 Isabelle, and HOL.  
 
 @menu
@@ -180,7 +180,7 @@ Isabelle, and HOL.
 * Coq Proof General::           
 * Isabelle Proof General::    
 * HOL Proof General::
-@c * AF2 Proof General::
+@c * PhoX Proof General::
 * Obtaining and Installing::  
 * Known bugs and workarounds::  
 * References::                  
@@ -288,10 +288,11 @@ proving theorems.
 Adapting for new proof assistants continues to be made more flexible,
 and easier in several places.  This has been motivated by adding
 experimental support for some new systems.  One new system which had
-good support added in a very short space of time is @b{AF2}
-(see @uref{http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html, the AF2 home page}
-for more information).  AF2 joins the rank of officially supported
-Proof General instances, thanks to its developer Christophe Raffalli.
+good support added in a very short space of time is @b{PhoX} (see
+@uref{http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html, the PhoX home
+page} for more information).  PhoX joins the rank of officially
+supported Proof General instances, thanks to its developer Christophe
+Raffalli.
 
 Breaking the manual into two pieces was overdue: now all details on
 adapting Proof General, and notes on its internals, are in the
-- 
cgit v1.2.3