[
Top
]
[
Contents
]
[
Index
]
[
?
]
Table of Contents
Introduction
Future
Credits
1. Beginning with a New Prover
1.1 Overview of adding a new prover
1.2 Demonstration instance and easy configuration
1.3 Major modes used by Proof General
2. Menus, toolbar, and user-level commands
2.1 Settings for generic user-level commands
2.2 Menu configuration
2.3 Toolbar configuration
3. Proof Script Settings
3.1 Recognizing commands and comments
3.2 Recognizing proofs
3.3 Recognizing other elements
3.4 Configuring undo behaviour
3.5 Nested proofs
3.6 Safe (state-preserving) commands
3.7 Activate scripting hook
3.8 Automatic multiple files
3.9 Completions
4. Proof Shell Settings
4.1 Commands
4.2 Script input to the shell
4.3 Settings for matching various output from proof process
4.4 Settings for matching urgent messages from proof process
4.5 Hooks and other settings
5. Goals Buffer Settings
6. Splash Screen Settings
7. Global Constants
8. Handling Multiple Files
9. Configuring Editing Syntax
10. Configuring Font Lock
11. Configuring X-Symbol
12. Writing More Lisp Code
12.1 Default values for generic settings
12.2 Adding prover-specific configurations
12.3 Useful variables
12.4 Useful functions and macros
13. Internals of Proof General
13.1 Spans
13.2 Proof General site configuration
13.3 Configuration variable mechanisms
13.4 Global variables
13.5 Proof script mode
13.6 Proof shell mode
13.6.1 Input to the shell
13.6.2 Output from the shell
13.7 Debugging
A. Plans and Ideas
A.1 Proof by pointing and similar features
A.2 Granularity of atomic command sequences
A.3 Browser mode for script files and theories
B. Demonstration Instantiations
B.1 demoisa-easy.el
B.2 demoisa.el
Function and Command Index
Variable and User Option Index
Concept Index
[
Top
]
[
Contents
]
[
Index
]
[
?
]
This document was generated by
David Aspinall
on
November, 7 2006
using
texi2html 1.76
.