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

Proof General

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

Proof General 4.6-git has been tested with GNU Emacs 25.2. It is supplied ready customized for the proof assistants Coq, EasyCrypt, qrhl-tool, and PhoX.

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. Configuring Proof-Tree Visualization  
13. Writing More Lisp Code  
14. 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 on April 20, 2024 using texi2html 1.82.