Table of Contents
- Preface
- 1. Introducing Proof General
- 2. Basic Script Management
- 3. Advanced Script Management and Editing
- 3.1 Document centred working
- 3.2 Automatic processing
- 3.3 Visibility of completed proofs
- 3.4 Switching between proof scripts
- 3.5 View of processed files
- 3.6 Retracting across files
- 3.7 Asserting across files
- 3.8 Proof status statistic
- 3.9 Automatic multiple file handling
- 3.10 Escaping script management
- 3.11 Editing features
- 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 Proof status statistic for Coq
- 10.7 Editing multiple proofs
- 10.8 User-loaded tactics
- 10.9 Indentation tweaking
- 10.10 Holes feature
- 10.11 Proof-Tree Visualization
- 10.12 Showing Proof Diffs
- 10.13 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 January 29, 2025 using texi2html 1.82.