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 EntrySection

A
active scripting bufferActive scripting buffer
AltPrerequisites for this manual
annotationDocument centred working
AssertionLocked queue and editing regions
AssertionAsserting across files
auto raiseDisplay customization
Automatic processingAutomatic processing
autosendAutomatic processing

B
blue textLocked queue and editing regions
buffer display customizationDisplay customization

C
CentaurHistory of Proof General
colourSyntax highlighting
completionSupport for completion
CtCoqHistory of Proof General
CustomizationCustomizing Proof General

D
Dedicated windowsUser options
display customizationDisplay customization

E
EasyCrypt Proof GeneralEasyCrypt Proof General
Editing regionLocked queue and editing regions
Emacs customization libraryHow to customize

F
FeaturesFeatures of Proof General
file variablesUsing file variables
font lockSyntax highlighting
framesDisplay customization
FutureFuture

G
genericHistory of Proof General
goalGoal-save sequences
goal-save sequencesGoal-save sequences
goals bufferSummary of Proof General buffers
Greek lettersUnicode symbols and special layout support

H
historyHistory of Proof General

I
ImenuImenu and Speedbar
IndentationUser options
index menuImenu and Speedbar
Input ringEditing features
Input ringUser options

K
key sequencesPrerequisites for this manual
keybindingsAdding your own keybindings

L
Locked regionLocked queue and editing regions
logical symbolsUnicode symbols and special layout support

M
maintenanceCredits
mathematical symbolsUnicode symbols and special layout support
Maths MenuUnicode symbols and special layout support
MetaPrerequisites for this manual
Multiple FilesAdvanced Script Management and Editing
multiple framesDisplay customization
multiple windowsDisplay customization

N
newsNews for Version 4.5
newsNews for Version 4.4
newsNews for Version 4.3
newsNews for Version 4.2
newsNews for Version 4.1
newsNews for Version 4.0
newsOld News for 3.1
newsOld News for 3.2

O
outline modeSupport for outline mode

P
pink textLocked queue and editing regions
prefix argumentScript processing commands
proof assistantIntroducing Proof General
proof by pointingSummary of Proof General buffers
proof by pointingHistory of Proof General
Proof GeneralIntroducing Proof General
Proof General KitFuture
proof scriptProof scripts
Proof script indentationUser options
proof script modeScript buffers
proof-tree visualizationGraphical Proof-Tree Visualization

Q
Query program nameUser options
Queue regionLocked queue and editing regions

R
Remote hostUser options
Remote shellUser options
response bufferSummary of Proof General buffers
RetractionLocked queue and editing regions
RetractionRetracting across files
Running proof assistant remotelyUser options

S
saveGoal-save sequences
script bufferScript buffers
script managementHistory of Proof General
scriptingProof scripts
ShellEscaping script management
shell bufferSummary of Proof General buffers
Shell Proof GeneralShell Proof General
SpeedbarImenu and Speedbar
Strict read-onlyUser options
structure editorHistory of Proof General
subscriptsUnicode symbols and special layout support
superscriptsUnicode symbols and special layout support
Switching between proof scriptsSwitching between proof scripts
symbolsUnicode symbols and special layout support

T
tagsSupport for tags
three-buffer interactionDisplay customization
Tokens ModeUnicode symbols and special layout support
Toolbar button enablersUser options
Toolbar disablingUser options
Toolbar follow modeUser options

U
Undo in read-only regionUser options
User optionsUser options
Using CustomizeHow to customize

V
Visibility of proofsVisibility of completed proofs

W
Why use Proof General?Features of Proof General

X
X-SymbolsUnicode symbols and special layout support