| Index Entry | Section |
|
A | | |
| active scripting buffer | 2.3.3 Active scripting buffer |
| Alt | 1.5 Prerequisites for this manual |
| Assertion | 2.3.1 Locked, queue, and editing regions |
| Assertion | 4.5 Asserting across files |
|
B | | |
| blue text | 2.3.1 Locked, queue, and editing regions |
| buffer display customization | 6.3 Display customization |
|
C | | |
| Centaur | History of Proof General |
| colour | 5.1 Syntax highlighting |
| completion | 5.6 Support for completion |
| CtCoq | History of Proof General |
| Customization | 6. Customizing Proof General |
|
D | | |
| Dedicated windows | 6.4 User options |
| display customization | 6.3 Display customization |
|
E | | |
| Editing region | 2.3.1 Locked, queue, and editing regions |
| Emacs customization library | 6.2 How to customize |
|
F | | |
| Features | 1.3 Features of Proof General |
| file variables | 7.2 Using file variables |
| font lock | 5.1 Syntax highlighting |
| frames | 6.3 Display customization |
| fume-func | 5.4 Imenu and Speedbar (and Function Menu) |
| func-menu | 5.4 Imenu and Speedbar (and Function Menu) |
| function menu | 5.4 Imenu and Speedbar (and Function Menu) |
| Future | Future |
|
G | | |
| generic | History of Proof General |
| goal | 2.3.2 Goal-save sequences |
| goal-save sequences | 2.3.2 Goal-save sequences |
| goals buffer | 2.4 Summary of Proof General buffers |
| Greek letters | 5.2 X-Symbol support |
| Greek letters | 5.3 Unicode support |
|
H | | |
| history | History of Proof General |
| HOL Proof General | 11. HOL Proof General |
|
I | | |
| Imenu | 5.4 Imenu and Speedbar (and Function Menu) |
| Indentation | 6.4 User options |
| index menu | 5.4 Imenu and Speedbar (and Function Menu) |
| Input ring | 4.8 Editing features |
| Input ring | 6.4 User options |
| Isabelle commands | 10.2 Isabelle commands |
| Isabelle customizations | 10.4 Isabelle customizations |
| Isabelle logic | 10.1 Choosing logic and starting isabelle |
| Isabelle Proof General | 10. Isabelle Proof General |
|
K | | |
| key sequences | 1.5 Prerequisites for this manual |
| keybindings | 7.1 Adding your own keybindings |
|
L | | |
| LEGO Proof General | 8. LEGO Proof General |
| lego-mode | Credits |
| lego-mode | History of Proof General |
| Locked region | 2.3.1 Locked, queue, and editing regions |
| logical symbols | 5.2 X-Symbol support |
| logical symbols | 5.3 Unicode support |
|
M | | |
| maintenance | Credits |
| mathematical symbols | 5.2 X-Symbol support |
| mathematical symbols | 5.3 Unicode support |
| Meta | 1.5 Prerequisites for this manual |
| Multiple Files | 4. Advanced Script Management and Editing |
| multiple frames | 6.3 Display customization |
| multiple windows | 6.3 Display customization |
|
N | | |
| news | Latest news for version 3.7.1 |
| news | Old News for 3.1 |
| news | Old News for 3.2 |
|
O | | |
| outline mode | 5.5 Support for outline mode |
|
P | | |
| pink text | 2.3.1 Locked, queue, and editing regions |
| prefix argument | 2.6 Script processing commands |
| proof assistant | 1. Introducing Proof General |
| proof by pointing | 2.4 Summary of Proof General buffers |
| proof by pointing | History of Proof General |
| Proof General | 1. Introducing Proof General |
| Proof General Kit | Future |
| proof script | 2.2 Proof scripts |
| Proof script indentation | 6.4 User options |
| proof script mode | 2.3 Script buffers |
|
Q | | |
| Query program name | 6.4 User options |
| Queue region | 2.3.1 Locked, queue, and editing regions |
|
R | | |
| Remote host | 6.4 User options |
| Remote shell | 6.4 User options |
| response buffer | 2.4 Summary of Proof General buffers |
| Retraction | 2.3.1 Locked, queue, and editing regions |
| Retraction | 4.4 Retracting across files |
| Running proof assistant remotely | 6.4 User options |
|
S | | |
| save | 2.3.2 Goal-save sequences |
| script buffer | 2.3 Script buffers |
| script management | History of Proof General |
| scripting | 2.2 Proof scripts |
| Shell | 4.7 Escaping script management |
| shell buffer | 2.4 Summary of Proof General buffers |
| Shell Proof General | 12. Shell Proof General |
| Speedbar | 5.4 Imenu and Speedbar (and Function Menu) |
| Strict read-only | 6.4 User options |
| structure editor | History of Proof General |
| Switching between proof scripts | 4.2 Switching between proof scripts |
| symbols | 5.2 X-Symbol support |
| symbols | 5.3 Unicode support |
|
T | | |
| tags | 5.7 Support for tags |
| three-buffer interaction | 6.3 Display customization |
| Toolbar button enablers | 6.4 User options |
| Toolbar disabling | 6.4 User options |
| Toolbar follow mode | 6.4 User options |
|
U | | |
| Undo in read-only region | 6.4 User options |
| User options | 6.4 User options |
| Using Customize | 6.2 How to customize |
|
V | | |
| Visibility of proofs | 4.1 Visibility of completed proofs |
|
W | | |
| Why use Proof General? | 1.3 Features of Proof General |
|
X | | |
| X-Symbols | 5.2 X-Symbol support |
| X-Symbols | 5.3 Unicode support |
|