Proof General

This file documents 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 on Linux. It is supplied ready to use for the proof assistants Coq, EasyCrypt, qrhl-tool, 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. Coq Proof General
11. EasyCrypt Proof General
12. 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

---

This document was generated on July 15, 2025 using texi2html 1.82.