blob: 3cade5efaad123c45f5f71e16e033626f5940044 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
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 Coq, Isabelle and LEGO. Details
are on the web at:
http://www.dcs.ed.ac.uk/home/proofgen/
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...
-- David Aspinall & Thomas Kleymann
(Please contact via proofgen@dcs.ed.ac.uk)
*******
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.
|
