Proof General --- Organize your proofs!
=======================================

Proof General is a generic Emacs interface for proof assistants.

This is version 3.2 of Proof General.   
(Check the About screen for precise version number).

The aim of the Proof General project is to provide a powerful and
configurable interfaces which help user-interaction with interactive
proof assistants.  Proof General targets power users rather than
novices, but we include general user interface niceties, such as
toolbar and menus, which make use easier for all.

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 feedback@proofgeneral.org

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 the subdirectories:

    acl2/   ACL2
     af2/   AF2
     coq/   Coq
 demoisa/   Demonstration instance for Isabelle
     isa/   Isabelle
    isar/   Isabelle/Isar
    lego/   LEGO
   hol98/   HOL 98

 generic/   Generic basis for Proof General

 plastic/   Plastic	[ in development release only ]
   twelf/   Twelf	[ in development release only ]
   pgkit/   PG Kit      [ in development release only ]


Check BUGS files for problems and issues, in this directory, and for
specific issues, in each prover subdirectory.  Please report bugs
not mentioned in any of these files to bugs@proofgeneral.org

For the latest news and downloads, or to join the user or developer
mailing list for Proof General, visit Proof General on the web 
at: http://www.proofgeneral.org

David Aspinall <da@proofgeneral.org>
October 2000.

-----

NEWSFLASH: Proof General has been Emacs based so far, but plans are
afoot to liberate it from the points and parentheses of Emacs Lisp.
The successor framework, Proof General Kit, proposes that proof assistants
use a *standard* XML-based protocol for interactive proof, dubbed
PGIP.  PGIP will allow a middleware layer for many interactive proof
tools and interface components (including Emacs).  The design of PGIP
was made possible by the present Emacs-based Proof General framework.  
For more on Proof General Kit, see http://www.proofgeneral.org/kit.html