[
Top
]
[
Contents
]
[
Index
]
[
?
]
Table of Contents
Preface
News for Version 4.0
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.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 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 Automatic multiple file handling
3.9 Escaping script management
3.10 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 Multiple File Support
10.2.1 Automatic Compilation in Detail
10.2.2 Locking Ancestors
10.2.3 Customizing Coq Multiple File Support
10.2.4 Current Limitations
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
Appendix A Obtaining and Installing
A.1 Obtaining Proof General
A.2 Installing Proof General from tarball
A.3 Setting the names of binaries
A.4 Notes for syssies
Byte compilation
Site-wide installation
Removing support for unwanted provers
Appendix 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
[
Top
]
[
Contents
]
[
Index
]
[
?
]
This document was generated on
September 16, 2013
using
texi2html 5.0
.