diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-10-13 17:00:52 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-10-13 17:00:52 +0000 |
| commit | c9a9a80cc82fcf4478a9146d97152fad5c4aefea (patch) | |
| tree | 5363e59fbc8edf16c0aff0f349209e52e33fe58a /etc | |
| parent | d33c54be6cf5c3a06cab73ea01308ed639876702 (diff) | |
Updated to posted version
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/announce | 41 |
1 files changed, 23 insertions, 18 deletions
diff --git a/etc/announce b/etc/announce index 8ec39188..3cade5ef 100644 --- a/etc/announce +++ b/etc/announce @@ -1,30 +1,35 @@ -From: Proof General maintainer <proofgen@dcs.ed.ac.uk> -To: coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, lego-club@dcs.ed.ac.uk -Subject: Generic Emacs interface for proof assistants - pre-release ---text follows this line-- +From: David Aspinall <da@dcs.ed.ac.uk> +To: coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, lego-club@dcs.ed.ac.uk +Subject: Proof General --- pre-release +Date: Tue, 13 Oct 1998 18:01:23 +0100 (BST) Proof General is a generic Emacs interface for proof assistants. It is -supplied ready-customised for the systems +supplied ready-customised for Coq, Isabelle and LEGO. Details +are on the web at: - Coq, Isabelle and LEGO + http://www.dcs.ed.ac.uk/home/proofgen/ -The code is designed to be generic, so you can adapt Proof General to -other proof assistants if you know a little bit of Emacs Lisp. It -supports script management, a toolbar, fontification, tags, function -menu, multiple files and remote proof assistants. +The interface supports script management, a toolbar, fontification, +tags, function menu, multiple files and remote proof assistants. +The code is designed to be adaptable to other proof assistants, by +writing a little bit of Emacs Lisp. Proof General and its instantiations were written by David Aspinall, Healfdene Goguen, Thomas Kleymann and Dilip Sequeira with help from Yves Bertot and using ideas from Project CROAP. -This is the first official pre-release and an ideal opportunity -for interested users to give us feedback at an early stage. Don't -forget to tell us which version you are testing. Improvements are -being made while you read this message... - -Further information and the sources are available from +This is the first official pre-release and an ideal opportunity for +interested users to give us feedback at an early stage. Don't forget +to tell us which version you are testing. Improvements are being made +while you read this message... - http://www.dcs.ed.ac.uk/home/proofgen/ + -- David Aspinall & Thomas Kleymann + (Please contact via proofgen@dcs.ed.ac.uk) +******* -David Aspinall & Thomas Kleymann
\ No newline at end of file +P.S. for Isabelle users: this interface provides slightly different +features to Isamode. One idea behind script management is that +interaction is centred on the script rather than the shell buffer. +In the future Isamode may be combined with Proof General, or Isamode +may be extended to offer script management. |