From 51c518b58fea79104daa1fabddfa4d338448f341 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 13 Apr 2004 12:58:18 +0000 Subject: Mention new instances of PG. --- CHANGES | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'CHANGES') 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 . +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. -- cgit v1.2.3