[Top] [Contents] [Index] [ ? ]

Proof General

 
START-INFO-DIR-ENTRY 
* Adapting Proof General: (PG-adapting).  Adapt Proof General to new provers
END-INFO-DIR-ENTRY

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

Proof General 3.7 has been tested with XEmacs 21.5.28 and GNU Emacs 22.1.1. 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.

Introduction  
1. Beginning with a New Prover  
2. Menus, toolbar, and user-level commands  
3. Proof Script Settings  
4. Proof Shell Settings  
5. Goals Buffer Settings  
6. Splash Screen Settings  
7. Global Constants  
8. Handling Multiple Files  
9. Configuring Editing Syntax  
10. Configuring Font Lock  
11. Configuring X-Symbol  
12. Writing More Lisp Code  
13. Internals of Proof General  
A. Plans and Ideas  
B. Demonstration Instantiations  
Function and Command Index  
Variable and User Option Index  
Concept Index  
[Top] [Contents] [Index] [ ? ]

This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.