Previous:
Keystroke Index
, Up:
Top
[
Contents
][
Index
]
Concept Index
Jump to:
A
B
C
D
E
F
G
H
I
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Index Entry
Section
A
active scripting buffer
:
Active scripting buffer
Alt
:
Prerequisites for this manual
annotation
:
Document centred working
Assertion
:
Locked queue and editing regions
Assertion
:
Asserting across files
auto raise
:
Display customization
Automatic processing
:
Automatic processing
autosend
:
Automatic processing
B
blue text
:
Locked queue and editing regions
buffer display customization
:
Display customization
C
Centaur
:
History of Proof General
colour
:
Syntax highlighting
completion
:
Support for completion
CtCoq
:
History of Proof General
Customization
:
Customizing Proof General
D
Dedicated windows
:
User options
display customization
:
Display customization
E
Editing region
:
Locked queue and editing regions
Emacs customization library
:
How to customize
F
Features
:
Features of Proof General
file variables
:
Using file variables
font lock
:
Syntax highlighting
frames
:
Display customization
Future
:
Future
G
generic
:
History of Proof General
goal
:
Goal-save sequences
goal-save sequences
:
Goal-save sequences
goals buffer
:
Summary of Proof General buffers
Greek letters
:
Unicode symbols and special layout support
H
history
:
History of Proof General
HOL Light Proof General
:
HOL Light Proof General
I
Imenu
:
Imenu and Speedbar
Indentation
:
User options
index menu
:
Imenu and Speedbar
Input ring
:
Editing features
Input ring
:
User options
Isabelle commands
:
Isabelle commands
Isabelle customizations
:
Isabelle customizations
Isabelle logic
:
Choosing logic and starting isabelle
Isabelle Proof General
:
Isabelle Proof General
K
key sequences
:
Prerequisites for this manual
keybindings
:
Adding your own keybindings
L
LEGO Proof General
:
LEGO Proof General
lego-mode
:
Credits
lego-mode
:
History of Proof General
Locked region
:
Locked queue and editing regions
logical symbols
:
Unicode symbols and special layout support
M
maintenance
:
Credits
mathematical symbols
:
Unicode symbols and special layout support
Maths Menu
:
Unicode symbols and special layout support
Meta
:
Prerequisites for this manual
Multiple Files
:
Advanced Script Management and Editing
multiple frames
:
Display customization
multiple windows
:
Display customization
N
news
:
News for Version 4.4
news
:
News for Version 4.3
news
:
News for Version 4.2
news
:
News for Version 4.1
news
:
News for Version 4.0
news
:
Old News for 3.1
news
:
Old News for 3.2
O
outline mode
:
Support for outline mode
P
pink text
:
Locked queue and editing regions
prefix argument
:
Script processing commands
proof assistant
:
Introducing Proof General
proof by pointing
:
Summary of Proof General buffers
proof by pointing
:
History of Proof General
Proof General
:
Introducing Proof General
Proof General Kit
:
Future
proof script
:
Proof scripts
Proof script indentation
:
User options
proof script mode
:
Script buffers
proof-tree visualization
:
Graphical Proof-Tree Visualization
Q
Query program name
:
User options
Queue region
:
Locked queue and editing regions
R
Remote host
:
User options
Remote shell
:
User options
response buffer
:
Summary of Proof General buffers
Retraction
:
Locked queue and editing regions
Retraction
:
Retracting across files
Running proof assistant remotely
:
User options
S
save
:
Goal-save sequences
script buffer
:
Script buffers
script management
:
History of Proof General
scripting
:
Proof scripts
Shell
:
Escaping script management
shell buffer
:
Summary of Proof General buffers
Shell Proof General
:
Shell Proof General
Speedbar
:
Imenu and Speedbar
Strict read-only
:
User options
structure editor
:
History of Proof General
subscripts
:
Unicode symbols and special layout support
superscripts
:
Unicode symbols and special layout support
Switching between proof scripts
:
Switching between proof scripts
symbols
:
Unicode symbols and special layout support
T
tags
:
Support for tags
three-buffer interaction
:
Display customization
Tokens Mode
:
Unicode symbols and special layout support
Toolbar button enablers
:
User options
Toolbar disabling
:
User options
Toolbar follow mode
:
User options
U
Undo in read-only region
:
User options
User options
:
User options
Using Customize
:
How to customize
V
Visibility of proofs
:
Visibility of completed proofs
W
Why use Proof General?
:
Features of Proof General
X
X-Symbols
:
Unicode symbols and special layout support
Jump to:
A
B
C
D
E
F
G
H
I
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Table of Contents
Preface
News for Version 4.4
News for Version 4.3
News for Version 4.2
News for Version 4.1
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 Graphical Proof-Tree Visualization
7.1 Starting and Stopping Proof-Tree Visualization
7.2 Features of Prooftree
7.3 Prooftree Customization
8 Customizing Proof General
8.1 Basic options
8.2 How to customize
8.3 Display customization
8.4 User options
8.5 Changing faces
8.5.1 Script buffer faces
8.5.2 Goals and response faces
8.6 Tweaking configuration settings
9 Hints and Tips
9.1 Adding your own keybindings
9.2 Using file variables
9.3 Using abbreviations
10 LEGO Proof General
10.1 LEGO specific commands
10.2 LEGO tags
10.3 LEGO customizations
11 Coq Proof General
11.1 Coq-specific commands
11.2 Using the Coq project file
11.2.1 Changing the name of the coq project file
11.2.2 Disabling the coq project file mechanism
11.3 Multiple File Support
11.3.1 Automatic Compilation in Detail
11.3.2 Locking Ancestors
11.3.3 Quick compilation and .vio Files
11.3.4 Customizing Coq Multiple File Support
11.3.5 Current Limitations
11.4 Editing multiple proofs
11.5 User-loaded tactics
11.6 Holes feature
11.7 Proof-Tree Visualization
12 Isabelle Proof General
12.1 Choosing logic and starting isabelle
12.2 Isabelle commands
12.3 Isabelle settings
12.4 Isabelle customizations
13 HOL Light Proof General
14 Shell Proof General
Appendix A Obtaining and Installing
A.1 Obtaining Proof General
A.2 Installing Proof General from sources
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
Previous:
Keystroke Index
, Up:
Top
[
Contents
][
Index
]