Proof General: Table of Contents

Preface
- Latest news for version 3.7
- Future
- Credits
1. Introducing Proof General
- 1.1 Installing Proof General
- 1.2 Quick start guide
- 1.3 Features of Proof General
- 1.4 Supported proof assistants
- 1.5 Prerequisites for this manual
- 1.6 Organization of this manual
2. Basic Script Management
- 2.1 Walkthrough example in Isabelle
- 2.2 Proof scripts
- 2.3 Script buffers
- 2.4 Summary of Proof General buffers
- 2.5 Script editing commands
- 2.6 Script processing commands
- 2.7 Proof assistant commands
- 2.8 Toolbar commands
- 2.9 Interrupting during trace output
3. Subterm Activation and Proof by Pointing
- 3.1 Goals buffer commands
4. Advanced Script Management and Editing
- 4.1 Visibility of completed proofs
- 4.2 Switching between proof scripts
- 4.3 View of processed files
- 4.4 Retracting across files
- 4.5 Asserting across files
- 4.6 Automatic multiple file handling
- 4.7 Escaping script management
- 4.8 Editing features
- 4.9 Experimental features
5. Support for other Packages
- 5.1 Syntax highlighting
- 5.2 X-Symbol support
- 5.3 Unicode support
- 5.4 Imenu and Speedbar (and Function Menu)
- 5.5 Support for outline mode
- 5.6 Support for completion
- 5.7 Support for tags
6. Customizing Proof General
- 6.1 Basic options
- 6.2 How to customize
- 6.3 Display customization
- 6.4 User options
- 6.5 Changing faces
- 6.6 Tweaking configuration settings
7. Hints and Tips
- 7.1 Adding your own keybindings
- 7.2 Using file variables
- 7.3 Using abbreviations
8. LEGO Proof General
- 8.1 LEGO specific commands
- 8.2 LEGO tags
- 8.3 LEGO customizations
9. Coq Proof General
- 9.1 Coq-specific commands
- 9.2 Coq-specific variables
- 9.3 Editing multiple proofs
- 9.4 User-loaded tactics
- 9.5 Holes feature
10. Isabelle Proof General
- 10.1 Isabelle commands
- 10.2 Logics and Settings
- 10.3 Isabelle customizations
11. HOL Proof General
12. Shell Proof General
A. Obtaining and Installing
- A.1 Obtaining Proof General
- A.2 Installing Proof General from tarball
- A.3 Installing Proof General from RPM package
- A.4 Setting the names of binaries
- A.5 Notes for syssies
B. Bugs and Enhancements
References
History of Proof General
- Old News for 3.0
- Old News for 3.1
- Old News for 3.2
- Old News for 3.3
- Old News for 3.4
Function and Command Index
Variable and User Option Index
Keystroke Index
Concept Index

This document was generated by David Aspinall on January, 31 2008 using texi2html 1.78.

Proof General user manual

Table of Contents