Adapting Proof General

Proof General — Organize your proofs!


Adapting Proof General 4.1 to new provers

October 2011

proofgeneral.inf.ed.ac.uk

David Aspinall with T. Kleymann

This manual and the program Proof General are Copyright © 2000-2011 by members of the Proof General team, LFCS Edinburgh.



Permission is granted to make and distribute verbatim copies of this manual provided the copyright notice and this permission notice are preserved on all copies.



This manual documents Proof General, Version 4.1, for use GNU Emacs 23.3 or (as far as possible) later versions. Proof General is distributed under the terms of the GNU General Public License (GPL); please check the accompanying file ‘COPYING’ for more details.


Visit Proof General on the web at http://proofgeneral.inf.ed.ac.uk

Version control: PG-adapting.texi,v 11.15 2011/10/03 09:04:25 da Exp


[ < ] [ > ]   [Contents] [Index] [ ? ]

Proof General

This file documents configuration mechanisms for version 4.1 of Proof General, a generic Emacs interface for proof assistants.

Proof General 4.1 has been tested with GNU Emacs 23.3. It is supplied ready customized for the proof assistants Coq, Lego, Isabelle, and HOL.

This manual contains information for customizing to new proof assistants; see the user manual for details about how to use Proof General.


[ < ] [ > ]   [Contents] [Index] [ ? ]

This document was generated on September 25, 2013 using texi2html 5.0.