Table of Contents
- 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
- 10.1 Coq-specific commands
- 10.2 Using the Coq project file
- 10.3 Proof using annotations
- 10.4 Multiple File Support
- 10.5 Omitting proofs for speed
- 10.6 Editing multiple proofs
- 10.7 User-loaded tactics
- 10.8 Indentation tweaking
- 10.9 Holes feature
- 10.10 Proof-Tree Visualization
- 10.11 Showing Proof Diffs
- 10.12 Opam-switch-mode support
- 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 April 18, 2024 using texi2html 1.82.