Mention new instances of PG.

1 files changed, 16 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 637270aa..664b4b07 100644
--- a/CHANGES
+++ b/CHANGES
@@ -214,8 +214,23 @@ holes operation are available in the Coq/holes menu.
 
 Symbols are encoded only if between spaces or _'s. Sub/superscripts
 are now introduced by '__' and '^^' respectively, and the rest of the
-word is sub/superscripted. to put spaces inside sub/superscripts, use
+word is sub/superscripted.  To put spaces inside sub/superscripts, use
 _{...} or ^{...}. Notice that this syntax is not understood by Coq
 and you will need to defined it with the "Notation" command of Coq.
 
 
+** Additional instances of Proof General
+
+*** ccc:  Proof General for the Casl Consistency Checker
+
+Provided by Christoph Lüth <cxl@informatik.uni-bremen.de>.
+See http://www.informatik.uni-bremen.de/cofi/ccc for more information.
+
+*** pgshell:  Proof General for shell scripts/simple command interpreters.
+
+This instance of PG is handy just for using script management to
+cut-and-paste into a buffer running an ordinary shell or tool
+with a command-line interpreter of some kind.  
+
+Provides an instant and cheap interface to command-line interpreters,
+to avoid tiresomely using cut-and-paste to run pre-recorded commands.