[Top] [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.

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 Tokens  
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 Charlie & on July 21, 2012 using texi2html 1.82.