[
Top
]
[
Contents
]
[
Index
]
[
?
]
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.3.1 Locked, queue, and editing regions
2.3.2 Goal-save sequences
2.3.3 Active scripting buffer
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
Byte compilation
Site-wide installation
Removing support for unwanted provers
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
[
Top
]
[
Contents
]
[
Index
]
[
?
]
This document was generated by
David Aspinall
on
January, 31 2008
using
texi2html 1.78
.