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

Proof General

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

Proof General 4.5-git has been tested with GNU Emacs 24.3 on Linux. It is supplied ready to use for the proof assistants Coq, EasyCrypt, and PhoX.

Preface  
1. Introducing Proof General  
2. Basic Script Management  
3. Advanced Script Management and Editing  
4. Unicode symbols and special layout support  
5. Support for other Packages  
6. Subterm Activation and Proof by Pointing  
7. Graphical Proof-Tree Visualization  
8. Customizing Proof General  
9. Hints and Tips  
10. LEGO Proof General  
11. Coq Proof General  
12. Isabelle Proof General  
13. HOL Light Proof General  
14. EasyCrypt Proof General  
15. Shell Proof General  
A. Obtaining and Installing  
B. Bugs and Enhancements  
References  
History of Proof General  
Function and Command Index  
Variable and User Option Index  
Keystroke Index  
Concept Index  
[Top] [Contents] [Index] [ ? ]

This document was generated by Erik Martin-Dorel on April 2, 2020 using texi2html 1.82.