Proof General: Table of Contents

Preface
- News for Version 4.0
- 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. Advanced Script Management and Editing
- 3.1 Document centred working
- 3.2 Visibility of completed proofs
- 3.3 Switching between proof scripts
- 3.4 View of processed files
- 3.5 Retracting across files
- 3.6 Asserting across files
- 3.7 Automatic multiple file handling
- 3.8 Escaping script management
- 3.9 Editing features
4. Unicode symbols and special layout support
- 4.1 Maths menu
- 4.2 Unicode Tokens mode
- 4.3 Configuring tokens symbols and shortcuts
- 4.4 Special layout
- 4.5 Moving between Unicode and tokens
- 4.6 Finding available tokens shortcuts and symbols
- 4.7 Selecting suitable fonts
5. Support for other Packages
- 5.1 Syntax highlighting
- 5.2 Imenu and Speedbar
- 5.3 Support for outline mode
- 5.4 Support for completion
- 5.5 Support for tags
6. Subterm Activation and Proof by Pointing
- 6.1 Goals buffer commands
7. Customizing Proof General
- 7.1 Basic options
- 7.2 How to customize
- 7.3 Display customization
- 7.4 User options
- 7.5 Changing faces
  - 7.5.1 Script buffer faces
  - 7.5.2 Goals and response faces
- 7.6 Tweaking configuration settings
8. Hints and Tips
- 8.1 Adding your own keybindings
- 8.2 Using file variables
- 8.3 Using abbreviations
9. LEGO Proof General
- 9.1 LEGO specific commands
- 9.2 LEGO tags
- 9.3 LEGO customizations
10. Coq Proof General
- 10.1 Coq-specific commands
- 10.2 Coq-specific variables
- 10.3 Editing multiple proofs
- 10.4 User-loaded tactics
- 10.5 Holes feature
11. Isabelle Proof General
- 11.1 Choosing logic and starting isabelle
- 11.2 Isabelle commands
- 11.3 Isabelle settings
- 11.4 Isabelle customizations
12. HOL Proof General
13. 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
- Old News for 3.5
- Old News for 3.6
- Old News for 3.7
Function and Command Index
Variable and User Option Index
Keystroke Index
Concept Index

This document was generated by David Aspinall on December, 4 2009 using texi2html 1.78.

Proof General user manual (latest release)

Table of Contents