af2 is now called PhoX

9 files changed, 218 insertions, 218 deletions

diff --git a/README b/README
index bb381ac0..ba42bc4a 100644
--- a/README
+++ b/README
@@ -26,7 +26,7 @@ For notes on the supported assistants, see the README files
 in the subdirectories:
 
     acl2/   ACL2
-     af2/   AF2
+     af2/   PhoX
      coq/   Coq
  demoisa/   Demonstration instance for Isabelle
      isa/   Isabelle
diff --git a/af2/README b/af2/README
index 8d0f990f..9c955b84 100644
--- a/af2/README
+++ b/af2/README
@@ -1,4 +1,4 @@
-AF2 Proof General, for AF2.
+PhoX Proof General, for Phox.
 
 Written by Christophe Raffalli
 
@@ -6,13 +6,13 @@ $Id$
 
 Status:	       supported
 Maintainer:    Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr>
-AF2 version:   
-AF2 homepage:  http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html
+PhoX version:  0.7
+PhoX homepage:  http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html
 
 ========================================
 
-This mode has support for script management with AF2, and some
-other features ported from AF2's own Emacs mode.
+This mode has support for script management with PhoX, and some
+other features ported from PhoX's own Emacs mode.
 
 
 
diff --git a/af2/af2-outline.el b/af2/af2-outline.el
deleted file mode 100644
index e3dbf845..00000000
--- a/af2/af2-outline.el
+++ /dev/null
@@ -1,57 +0,0 @@
-;;--------------------------------------------------------------------------;;
-;;--------------------------------------------------------------------------;;
-;;                      PARAMÉTRAGE du MODE outline
-;;--------------------------------------------------------------------------;;
-
-
-(setq af2-outline-title-regexp "\\((\\*[ \t\n]*title =\\)")
-(setq af2-outline-section-regexp "\\((\\*\\*+\\)")
-(setq af2-outline-save-regexp "\\((\\*#\\)")
-(setq 
- af2-outline-theo-regexp 
- "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)")
-(setq 
- af2-outline-theo2-regexp 
- "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)")
-
-(setq 
-  af2-outline-regexp 
-  (concat 
-   af2-outline-title-regexp "\\|" 
-   af2-outline-section-regexp "\\|" 
-   af2-outline-save-regexp "\\|" 
-   af2-outline-theo-regexp "\\|" 
-   af2-outline-theo2-regexp))
-
-(setq af2-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)")
-
-;(if af2-outline
-;    (add-hook 'af2-mode-hook '(lambda()(outline-minor-mode 1)))
-;  )
-
-(defun af2-outline-level()
-  "Find the level of current outline heading in some af2 libraries."
-  (let ((retour 0))
-    (save-excursion
-      (cond ((looking-at af2-outline-title-regexp) 1)
-	    ((looking-at af2-outline-section-regexp)
-	     (min 6 (- (match-end 0) (match-beginning 0)))) ; valeur maxi 6
-	    ((looking-at af2-outline-theo-regexp) 7)
-	    ((looking-at  (concat af2-outline-save-regexp "\\|"
-				 af2-outline-theo2-regexp )
-			 ) 8)
-	    )
-      )))
-
-(defun af2-setup-outline ()
-  "Set up local variable for outline mode"
-  (make-local-variable 'outline-heading-end-regexp)
-  (setq outline-heading-end-regexp af2-outline-heading-end-regexp)
-  (make-local-variable 'outline-regexp)
-  (setq outline-regexp af2-outline-regexp)
-  (make-local-variable 'outline-level)
-  (setq outline-level 'af2-outline-level)
-  (outline-minor-mode 1)
-)
-
-(provide 'af2-outline)
\ No newline at end of file
diff --git a/af2/af2-font.el b/af2/phox-font.el
index 0a67826d..f04844fa 100644
--- a/af2/af2-font.el
+++ b/af2/phox-font.el
@@ -3,7 +3,7 @@
 ;;                       Font lock keywords
 ;;--------------------------------------------------------------------------;;
 
-(defconst af2-font-lock-keywords
+(defconst phox-font-lock-keywords
   (list
 ;commands
    '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)"
@@ -111,7 +111,7 @@
 
 ;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be
 ;; used to determine the symbol character codes.
-(defvar af2-sym-lock-keywords
+(defvar phox-sym-lock-keywords
   '((">=" 0 1 179)
     ("<=" 0 1 163)
     ("!=" 0 1 185)
@@ -125,14 +125,14 @@
     ("-->" 0 1 222)
     ("->" 0 1 174)
     ("~" 0 1 216))
-  "If non nil: Overrides default Sym-Lock patterns for Af2.")
+  "If non nil: Overrides default Sym-Lock patterns for PhoX.")
 
-(defun af2-sym-lock-start ()
-	(if (and (featurep 'sym-lock) af2-sym-lock)
+(defun phox-sym-lock-start ()
+	(if (and (featurep 'sym-lock) phox-sym-lock)
 	    (progn
 	      (setq sym-lock-color
 		    (face-foreground 'font-lock-function-name-face))
 	      (if (not sym-lock-keywords)
-		  (sym-lock af2-sym-lock-keywords)))))
+		  (sym-lock phox-sym-lock-keywords)))))
 
-(provide 'af2-font)
+(provide 'phox-font)
diff --git a/af2/af2-fun.el b/af2/phox-fun.el
index d03c23ab..58771057 100644
--- a/af2/af2-fun.el
+++ b/af2/phox-fun.el
@@ -5,15 +5,15 @@
 ;; note : program extraction is still experimental
 ;;--------------------------------------------------------------------------;;
 
-(defun af2-compile-theorem(name)
+(defun phox-compile-theorem(name)
   "Interactive function : 
-ask for the name of a theorem and send a compile command to af2 for it."
+ask for the name of a theorem and send a compile command to PhoX for it."
   (interactive "stheorem : ")
   (proof-shell-invisible-command (concat "compile " name ".\n")))
 
-(defun af2-compile-theorem-around-point()
+(defun phox-compile-theorem-around-point()
 "Interactive function : 
-send a compile command to af2 for the theorem which name is under the cursor."
+send a compile command to PhoX for the theorem which name is under the cursor."
   (interactive)
   (let (start end)
     (save-excursion
@@ -21,42 +21,42 @@ send a compile command to af2 for the theorem which name is under the cursor."
       (setq start (point))
       (forward-word -1)
       (setq end (point)))
-    (af2-compile-theorem (buffer-substring start end))))
+    (phox-compile-theorem (buffer-substring start end))))
 
 
 (setq
- af2-forget-id-command "del %s.\n"
- af2-forget-new-elim-command "edel elim %s.\n"
- af2-forget-new-intro-command "edel intro %s.\n"
- af2-forget-new-rewrite-command "edel rewrite %s.\n"
- af2-forget-close-def-command "edel closed %s.\n"
- af2-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
- af2-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)"
- af2-spaces-regexp "[ \n\t\r]*"
- af2-sy-definition-regexp (concat 
+ phox-forget-id-command "del %s.\n"
+ phox-forget-new-elim-command "edel elim %s.\n"
+ phox-forget-new-intro-command "edel intro %s.\n"
+ phox-forget-new-rewrite-command "edel rewrite %s.\n"
+ phox-forget-close-def-command "edel closed %s.\n"
+ phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
+ phox-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)"
+ phox-spaces-regexp "[ \n\t\r]*"
+ phox-sy-definition-regexp (concat 
    "\\(Cst\\|def\\)"
-   af2-comments-regexp
+   phox-comments-regexp
    "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
- af2-definition-regexp (concat
+ phox-definition-regexp (concat
    "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)"
-   af2-comments-regexp
-   af2-ident-regexp)
- af2-new-elim-regexp (concat
+   phox-comments-regexp
+   phox-ident-regexp)
+ phox-new-elim-regexp (concat
    "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
-   af2-ident-regexp)
- af2-new-intro-regexp (concat
+   phox-ident-regexp)
+ phox-new-intro-regexp (concat
    "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
-   af2-ident-regexp)
- af2-new-rewrite-regexp (concat
+   phox-ident-regexp)
+ phox-new-rewrite-regexp (concat
    "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
-   af2-ident-regexp)
- af2-close-def-regexp (concat
+   phox-ident-regexp)
+ phox-close-def-regexp (concat
    "close_def"
-   af2-comments-regexp
+   phox-comments-regexp
    "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]")
 )
 
-(defun af2-find-and-forget (span)
+(defun phox-find-and-forget (span)
   (let (str ans tmp (lsp -1))
     (while span 
       (setq str (span-property span 'cmd))
@@ -66,36 +66,36 @@ send a compile command to af2 for the theorem which name is under the cursor."
        ((eq (span-property span 'type) 'comment))       
 
        ((eq (span-property span 'type) 'goalsave)
-	(setq ans (concat (format af2-forget-id-command
+	(setq ans (concat (format phox-forget-id-command
 				  (span-property span 'name)) ans)))
 
-       ((proof-string-match af2-new-elim-regexp str)
+       ((proof-string-match phox-new-elim-regexp str)
 	(setq ans 
-	      (concat (format af2-forget-new-elim-command 
+	      (concat (format phox-forget-new-elim-command 
 				  (match-string 3 str)) ans)))
 
-       ((proof-string-match af2-new-intro-regexp str)
+       ((proof-string-match phox-new-intro-regexp str)
 	(setq ans 
-	      (concat (format af2-forget-new-intro-command 
+	      (concat (format phox-forget-new-intro-command 
 				  (match-string 3 str)) ans)))
 
-       ((proof-string-match af2-new-rewrite-regexp str)
+       ((proof-string-match phox-new-rewrite-regexp str)
 	(setq ans 
-	      (concat (format af2-forget-new-rewrite-command 
+	      (concat (format phox-forget-new-rewrite-command 
 				  (match-string 3 str)) ans)))
 
-       ((proof-string-match af2-close-def-regexp str)
+       ((proof-string-match phox-close-def-regexp str)
 	(setq ans 
-	      (concat (format af2-forget-close-def-command 
+	      (concat (format phox-forget-close-def-command 
 				  (match-string 4 str)) ans)))
 
-       ((proof-string-match af2-sy-definition-regexp str)
+       ((proof-string-match phox-sy-definition-regexp str)
 	(setq ans 
-	      (concat (format af2-forget-id-command 
+	      (concat (format phox-forget-id-command 
 				  (concat "$" (match-string 7 str))) ans)))
 
-       ((proof-string-match af2-definition-regexp str)
-	(setq ans (concat (format af2-forget-id-command 
+       ((proof-string-match phox-definition-regexp str)
+	(setq ans (concat (format phox-forget-id-command 
 				      (match-string 6 str)) ans))))
 
 
@@ -111,15 +111,15 @@ send a compile command to af2 for the theorem which name is under the cursor."
 ;;--------------------------------------------------------------------------;;
 
 
-(defun af2-delete-symbol(symbol)
+(defun phox-delete-symbol(symbol)
   "Interactive function : 
-ask for a symbol and send a delete command to af2 for it."
+ask for a symbol and send a delete command to PhoX for it."
   (interactive "ssymbol : ")
   (proof-shell-invisible-command (concat "del " symbol ".\n")))
 
-(defun af2-delete-symbol-around-point()
+(defun phox-delete-symbol-around-point()
 "Interactive function : 
-send a delete command to af2 for the symbol whose name is under the cursor."
+send a delete command to PhoX for the symbol whose name is under the cursor."
   (interactive)
   (let (start end)
     (save-excursion
@@ -128,13 +128,13 @@ send a delete command to af2 for the symbol whose name is under the cursor."
       (forward-word 1)
       (setq end (point)))
     (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1)))
-    (af2-delete-symbol (buffer-substring start end))))
+    (phox-delete-symbol (buffer-substring start end))))
 
 ;;
 ;; Doing commands
 ;;
 
-(defun af2-assert-next-command-interactive ()
+(defun phox-assert-next-command-interactive ()
   "Process until the end of the next unprocessed command after point.
 If inside a comment, just process until the start of the comment."
   (interactive)
@@ -146,5 +146,5 @@ If inside a comment, just process until the start of the comment."
     (proof-assert-next-command))
    (proof-maybe-follow-locked-end)))
 
-(provide 'af2-fun)
+(provide 'phox-fun)
 
diff --git a/af2/phox-outline.el b/af2/phox-outline.el
new file mode 100644
index 00000000..766bddb3
--- /dev/null
+++ b/af2/phox-outline.el
@@ -0,0 +1,57 @@
+;;--------------------------------------------------------------------------;;
+;;--------------------------------------------------------------------------;;
+;;                      PARAMÉTRAGE du MODE outline
+;;--------------------------------------------------------------------------;;
+
+
+(setq phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)")
+(setq phox-outline-section-regexp "\\((\\*\\*+\\)")
+(setq phox-outline-save-regexp "\\((\\*#\\)")
+(setq 
+ phox-outline-theo-regexp 
+ "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)")
+(setq 
+ phox-outline-theo2-regexp 
+ "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)")
+
+(setq 
+  phox-outline-regexp 
+  (concat 
+   phox-outline-title-regexp "\\|" 
+   phox-outline-section-regexp "\\|" 
+   phox-outline-save-regexp "\\|" 
+   phox-outline-theo-regexp "\\|" 
+   phox-outline-theo2-regexp))
+
+(setq phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)")
+
+;(if phox-outline
+;    (add-hook 'phox-mode-hook '(lambda()(outline-minor-mode 1)))
+;  )
+
+(defun phox-outline-level()
+  "Find the level of current outline heading in some PhoX libraries."
+  (let ((retour 0))
+    (save-excursion
+      (cond ((looking-at phox-outline-title-regexp) 1)
+	    ((looking-at phox-outline-section-regexp)
+	     (min 6 (- (match-end 0) (match-beginning 0)))) ; valeur maxi 6
+	    ((looking-at phox-outline-theo-regexp) 7)
+	    ((looking-at  (concat phox-outline-save-regexp "\\|"
+				 phox-outline-theo2-regexp )
+			 ) 8)
+	    )
+      )))
+
+(defun phox-setup-outline ()
+  "Set up local variable for outline mode"
+  (make-local-variable 'outline-heading-end-regexp)
+  (setq outline-heading-end-regexp phox-outline-heading-end-regexp)
+  (make-local-variable 'outline-regexp)
+  (setq outline-regexp phox-outline-regexp)
+  (make-local-variable 'outline-level)
+  (setq outline-level 'phox-outline-level)
+  (outline-minor-mode 1)
+)
+
+(provide 'phox-outline)
\ No newline at end of file
diff --git a/af2/af2-tags.el b/af2/phox-tags.el
index 1c60b631..f2b5959a 100644
--- a/af2/af2-tags.el
+++ b/af2/phox-tags.el
@@ -15,7 +15,7 @@
 
 (require 'etags) 
 
-(defun af2-tags-add-table(table)
+(defun phox-tags-add-table(table)
   "add tags table"
   (interactive "D directory, location of a file named TAGS to add : ")
   (if proof-running-on-XEmacs
@@ -32,7 +32,7 @@
     )
   )
 
-(defun af2-tags-reset-table()
+(defun phox-tags-reset-table()
   "Set tags-table-list to nil."
   (interactive)
 ;  (make-local-variable 'tags-table-list)
@@ -42,28 +42,28 @@
     (setq tags-table-list nil))
   )
 
-(defun af2-tags-add-doc-table()
+(defun phox-tags-add-doc-table()
   "Add tags in text documentation."
   (interactive)
-  (af2-tags-add-table (concat af2-doc-dir "/text/TAGS"))
+  (phox-tags-add-table (concat phox-doc-dir "/text/TAGS"))
   )
 
-(defun af2-tags-add-lib-table()
+(defun phox-tags-add-lib-table()
   "Add tags in libraries."
   (interactive)
-  (af2-tags-add-table (concat af2-lib-dir "TAGS"))
+  (phox-tags-add-table (concat phox-lib-dir "TAGS"))
   )
  
-(defun af2-tags-add-local-table()
-  "Add the tags table created with function af2-create-local-table."
+(defun phox-tags-add-local-table()
+  "Add the tags table created with function phox-create-local-table."
   (interactive)
-  (af2-tags-add-table (concat buffer-file-name "TAGS"))
+  (phox-tags-add-table (concat buffer-file-name "TAGS"))
   )
 
-(defun af2-tags-create-local-table()
+(defun phox-tags-create-local-table()
   "create table on local buffer"
   (interactive)
-  (shell-command (concat af2-etags 
+  (shell-command (concat phox-etags 
 			 " -o " 
 			 (file-name-nondirectory (buffer-file-name))
 			 "TAGS "
@@ -72,6 +72,6 @@
 
 ;; default
 
-(if af2-tags-doc (add-hook 'af2-mode-hook 'af2-tags-add-doc-table))
+(if phox-tags-doc (add-hook 'phox-mode-hook 'phox-tags-add-doc-table))
 
-(provide 'af2-tags)
\ No newline at end of file
+(provide 'phox-tags)
\ No newline at end of file
diff --git a/af2/af2.el b/af2/phox.el
index 38f423cf..49f4ab15 100644
--- a/af2/af2.el
+++ b/af2/phox.el
@@ -3,11 +3,11 @@
 ;; Adjust toolbar entries.  (Must be done
 ;; before proof-toolbar is loaded).
 
-(if proof-running-on-XEmacs (setq af2-toolbar-entries
-      (remassoc 'context af2-toolbar-entries)))
+(if proof-running-on-XEmacs (setq phox-toolbar-entries
+      (remassoc 'context phox-toolbar-entries)))
 
 
-;; ======== User settings for Af2 ========
+;; ======== User settings for PhoX ========
 ;;
 ;; Defining variables using customize is pretty easy.
 ;; You should do it at least for your prover-specific user options.
@@ -15,84 +15,84 @@
 ;; proof-site provides us with two customization groups
 ;; automatically:  (based on the name of the assistant)
 ;;
-;; 'af2        -  User options for Af2 Proof General
-;; 'af2-config -  Configuration of Af2 Proof General
+;; 'phox        -  User options for PhoX Proof General
+;; 'phox-config -  Configuration of PhoX Proof General
 ;;			   (constants, but may be nice to tweak)
 ;;
 ;; The first group appears in the menu
-;;   ProofGeneral -> Customize -> Af2 
+;;   ProofGeneral -> Customize -> PhoX 
 ;; The second group appears in the menu:
-;;   ProofGeneral -> Internals -> Af2 config
+;;   ProofGeneral -> Internals -> PhoX config
 ;;
 
-(defcustom af2-prog-name "af2 -pg"
-  "*Name of program to run Af2."
+(defcustom phox-prog-name "phox -pg"
+  "*Name of program to run PhoX."
   :type 'file
-  :group 'af2)
+  :group 'phox)
 
-(defcustom af2-sym-lock t
+(defcustom phox-sym-lock t
   "*Whether to use sym-lock or not."
   :type 'boolean
-  :group 'af2)
+  :group 'phox)
 
-(defcustom af2-web-page
-  "http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html"
-  "URL of web page for Af2."
+(defcustom phox-web-page
+  "http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html"
+  "URL of web page for PhoX."
   :type 'string
-  :group 'af2-config)
+  :group 'phox-config)
 
-(defcustom af2-doc-dir 
-  "/usr/local/doc/af2"
-  "The name of the root documentation directory for af2."
+(defcustom phox-doc-dir 
+  "/usr/local/doc/phox"
+  "The name of the root documentation directory for PhoX."
   :type 'string
-  :group 'af2-config)
+  :group 'phox-config)
 
-(defcustom af2-lib-dir 
-  "/usr/local/lib/af2"
-  "The name of the root directory for af2 libraries."
+(defcustom phox-lib-dir 
+  "/usr/local/lib/phox"
+  "The name of the root directory for PhoX libraries."
   :type 'string
-  :group 'af2-config)
+  :group 'phox-config)
 
-(defcustom af2-tags-program 
-  (concat af2-doc-dir "/tools/af2_etags.sh")
+(defcustom phox-tags-program 
+  (concat phox-doc-dir "/tools/phox_etags.sh")
   "Program to run to generate TAGS table for proof assistant."
   :type 'string
-  :group 'af2-config)
+  :group 'phox-config)
 
-(defcustom af2-tags-doc 
+(defcustom phox-tags-doc 
   t
-  "*If non nil, tags table for af2 text documentation is loaded."
+  "*If non nil, tags table for PhoX text documentation is loaded."
   :type 'boolean
-  :group 'af2-config)
+  :group 'phox-config)
 
-(defcustom af2-etags 
-  (concat af2-doc-dir "/tools/af2_etags.sh")
+(defcustom phox-etags 
+  (concat phox-doc-dir "/tools/phox_etags.sh")
   "Command to build tags table."
   :type 'string
-  :group 'af2-config)
+  :group 'phox-config)
 
-(require 'af2-tags)
-(require 'af2-outline)
-(require 'af2-font)
-(require 'af2-fun)
+(require 'phox-tags)
+(require 'phox-outline)
+(require 'phox-font)
+(require 'phox-fun)
 
-;; ----- Af2 specific menu
+;; ----- PhoX specific menu
 
 (defpgdefault menu-entries
   '(    
-    ["Delete symbol around cursor" af2-delete-symbol-around-point t]
-    ["Delete symbol" af2-delete-symbol t]
-    ["Compile theorem under cursor" af2-compile-theorem-around-point t]
+    ["Delete symbol around cursor" phox-delete-symbol-around-point t]
+    ["Delete symbol" phox-delete-symbol t]
+    ["Compile theorem under cursor" phox-compile-theorem-around-point t]
     "----"
     ("Tags"
-     ["create a tags table for local buffer" af2-tags-create-local-table t]
+     ["create a tags table for local buffer" phox-tags-create-local-table t]
      ["------------------" nil nil]
-;    ["load table" af2-tags-load-table t]
-     ["add table"               af2-tags-add-table       t]
-     ["add local table"         af2-tags-add-local-table t]
-     ["add table for libraries" af2-tags-add-lib-table   t]
-     ["add table for text doc"  af2-tags-add-doc-table   t]
-     ["reset tags table list"   af2-tags-reset-table     t]
+;    ["load table" phox-tags-load-table t]
+     ["add table"               phox-tags-add-table       t]
+     ["add local table"         phox-tags-add-local-table t]
+     ["add table for libraries" phox-tags-add-lib-table   t]
+     ["add table for text doc"  phox-tags-add-doc-table   t]
+     ["reset tags table list"   phox-tags-reset-table     t]
      ["------------------" nil nil]
      ["Find theorem, definition ..." find-tag t]
      ["complete theorem, definition ..." complete-tag t]
@@ -103,8 +103,8 @@
 ;; ======== Configuration of generic modes ========
 ;;
 
-(defun af2-config ()
-  "Configure Proof General scripting for Af2."
+(defun phox-config ()
+  "Configure Proof General scripting for PhoX."
   (setq
    proof-terminal-char		?\.	; ends every command
    proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)"
@@ -115,14 +115,14 @@
    proof-save-command-regexp       "save"
    proof-goal-with-hole-regexp     (concat 
       "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)"
-      af2-comments-regexp
-      af2-ident-regexp)
+      phox-comments-regexp
+      phox-ident-regexp)
    proof-ignore-for-undo-count      "constraints\\|flags\\|goals\\|print\\|print_sort\\|eshow\\|search\\|priority\\|depend"
    proof-goal-with-hole-result     5
    proof-save-with-hole-regexp     (concat 
       "save"
-      af2-comments-regexp
-      af2-ident-regexp)
+      phox-comments-regexp
+      phox-ident-regexp)
    proof-save-with-hole-result     4
    proof-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror"
    proof-non-undoables-regexp      "undo"
@@ -131,19 +131,19 @@
    proof-kill-goal-command         "abort."
    proof-showproof-command         "goals."
    proof-undo-n-times-cmd          "undo %s."
-   proof-find-and-forget-fn        'af2-find-and-forget
+   proof-find-and-forget-fn        'phox-find-and-forget
    proof-find-theorems-command      "search \"%s\"."
    proof-auto-multiple-files       nil
-   font-lock-keywords              af2-font-lock-keywords 
+   font-lock-keywords              phox-font-lock-keywords 
    )
 )
 
-(defun af2-shell-config ()
-  "Configure Proof General shell for Af2."
+(defun phox-shell-config ()
+  "Configure Proof General shell for PhoX."
   (setq
    ;proof-shell-cd-cmd              "cd \"%s\""
-   proof-shell-prompt-pattern      "\\(>af2> \\)\\|\\(%af2% \\)"
-   proof-shell-annotated-prompt-regexp  "\\(>af2> \\)\\|\\(%af2% \\)"
+   proof-shell-prompt-pattern      "\\(>phox> \\)\\|\\(%phox% \\)"
+   proof-shell-annotated-prompt-regexp  "\\(>phox> \\)\\|\\(%phox% \\)"
    proof-shell-interrupt-regexp    "Interrupt"
    proof-shell-start-goals-regexp  "^Goals left to prove:"
    proof-shell-quit-cmd            "quit."
@@ -162,44 +162,44 @@
 ;; The derived modes set the variables, then call the
 ;; <mode>-config-done function to complete configuration.
 
-(define-derived-mode af2-mode proof-mode
-    "Af2 script" nil
-    (af2-config)
-    (af2-sym-lock-start)
+(define-derived-mode phox-mode proof-mode
+    "PhoX script" nil
+    (phox-config)
+    (phox-sym-lock-start)
     (proof-config-done)
-    (af2-setup-outline)
-    (define-key af2-mode-map [(control j)] 
-      'af2-assert-next-command-interactive)
+    (phox-setup-outline)
+    (define-key phox-mode-map [(control j)] 
+      'phox-assert-next-command-interactive)
     ;; with the previous binding,
     ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed"
 
-    (define-key af2-mode-map [(control c) (meta d)] 
-      'af2-delete-symbol-around-point)  
+    (define-key phox-mode-map [(control c) (meta d)] 
+      'phox-delete-symbol-around-point)  
     ;; Configure syntax table for block comments
     (modify-syntax-entry ?\* ". 23")
     (modify-syntax-entry ?\( "()1")
     (modify-syntax-entry ?\) ")(4"))
 
-(define-derived-mode af2-shell-mode proof-shell-mode
-   "Af2 shell" nil
-   (af2-shell-config)
+(define-derived-mode phox-shell-mode proof-shell-mode
+   "PhoX shell" nil
+   (phox-shell-config)
    (proof-shell-config-done))
 
-(define-derived-mode af2-response-mode proof-response-mode
-  "Af2 response" nil
+(define-derived-mode phox-response-mode proof-response-mode
+  "PhoX response" nil
   (setq 
-   font-lock-keywords  af2-font-lock-keywords
+   font-lock-keywords  phox-font-lock-keywords
    proof-output-fontify-enable     t)
-  (af2-sym-lock-start)
+  (phox-sym-lock-start)
   (proof-response-config-done)
   (font-lock-mode))
 
-(define-derived-mode af2-goals-mode proof-goals-mode
-  "Af2 goals" nil
+(define-derived-mode phox-goals-mode proof-goals-mode
+  "PhoX goals" nil
   (setq 
-   font-lock-keywords  af2-font-lock-keywords
+   font-lock-keywords  phox-font-lock-keywords
    proof-output-fontify-enable     t)
-  (af2-sym-lock-start)
+  (phox-sym-lock-start)
   (proof-goals-config-done)
   (font-lock-mode))
 
@@ -216,14 +216,14 @@
 ;; name of the program to run, and the modes for the shell, response,
 ;; and goals buffers.
 
-(add-hook 'proof-pre-shell-start-hook 'af2-pre-shell-start)
+(add-hook 'proof-pre-shell-start-hook 'phox-pre-shell-start)
 
-(defun af2-pre-shell-start ()
-  (setq proof-prog-name		af2-prog-name)
-  (setq proof-mode-for-shell    'af2-shell-mode)
-  (setq proof-mode-for-response 'af2-response-mode)
-  (setq proof-mode-for-goals	'af2-goals-mode))
+(defun phox-pre-shell-start ()
+  (setq proof-prog-name		phox-prog-name)
+  (setq proof-mode-for-shell    'phox-shell-mode)
+  (setq proof-mode-for-response 'phox-response-mode)
+  (setq proof-mode-for-goals	'phox-goals-mode))
 
-(provide 'af2)
+(provide 'phox)
 
 
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 3ddc2da4..84e91497 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -48,7 +48,7 @@
     (isa        "Isabelle"	"\\.ML$\\|\\.thy$")
     (lego	"LEGO"		"\\.l$")
     (coq	"Coq"		"\\.v$")
-    (af2	"Af2"		"\\.af2$")
+    (phox	"PhoX"		"\\.phx$")
     ;; The following provers are not fully supported, 
     ;; and have only preliminary support written 
     ;; (please volunteer to improve them!)