aboutsummaryrefslogtreecommitdiffhomepage
path: root/README
blob: 2e424556794f400c4d06db95270c8f466b607012 (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
36
37
38
39
40
41
42
Proof General --- Organize your proof with Emacs!
=================================================

Proof General is a generic Emacs interface for proof assistants.

Our aim is provide a powerful and configurable Emacs mode which helps
user-interaction with interactive proof assistants.

Please help us with this aim!  Configure Proof General for your proof
assistant, by adding features at the generic level wherever possible.
Send ideas, comments, patches, code to proofgen@dcs.ed.ac.uk.

See INSTALL for installation details.

See COPYING for license details.

See doc/ for documentation of Proof General.

For notes on the supported assistants, see the README files
in subdirectories:

     af2/   AF2
     coq/   Coq
     isa/   Isabelle
    isar/   Isabelle/Isar
    lego/   LEGO
   hol98/   HOL 98
 plastic/   Plastic	[ in development release only ]
 twelf/     Twelf	[ in development release only ]

Check BUGS for problems and issues, in this directory, and
for specific issues, in each prover subdirectory.

For the latest news and downloads, check the Proof General web page
at: http://www.proofgeneral.org


David Aspinall.
November 2000.