diff options
Diffstat (limited to 'README')
| -rw-r--r-- | README | 69 |
1 files changed, 69 insertions, 0 deletions
@@ -0,0 +1,69 @@ +Proof General --- Organize your proofs! +======================================= + +Proof General is a generic Emacs interface for proof assistants. + +This is version 3.3 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 REGISTER for registration information (please register). + +See doc/ for documentation of Proof General. + +For notes on the supported assistants, see the README files +in the subdirectories: + + acl2/ ACL2 + phox/ PhoX + coq/ Coq + demoisa/ Demonstration instance for Isabelle + hol98/ HOL 98 + isa/ Isabelle + isar/ Isabelle/Isar + lego/ LEGO + plastic/ Plastic + twelf/ Twelf + pgkit/ PG Kit [ in development release only ] + + generic/ Generic basis for Proof General + +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> +August 2001. + +----- + +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 + + + + + |