| Index Entry | | Section |
|
% | | |
| %abbrev | | 3.3 Definitions |
| %assert | | 10.1 Theorem Declaration |
| %block | | 9.1 Regular Worlds |
| %clause | | 5.7 Clause Definitions |
| %covers | | 9.2 Input Coverage |
| %establish | | 10.1 Theorem Declaration |
| %freeze | | 9.4 Subordination |
| %infix | | 3.4 Operator Declaration |
| %mode | | 7.1 Short Mode Declaration |
| %mode | | 7.2 Full Mode Declaration |
| %name | | 3.5 Name Preferences |
| %postfix | | 3.4 Operator Declaration |
| %prefix | | 3.4 Operator Declaration |
| %prove | | 10.1 Theorem Declaration |
| %query | | 5.1 Query Declaration |
| %querytabled | | 5.9 Tabled Logic Programming |
| %reduces | | 8.2 Reduction Declaration |
| %solve | | 5.2 Solve Declaration |
| %tabled | | 5.9 Tabled Logic Programming |
| %terminates | | 8.1 Termination Declaration |
| %theorem | | 10.1 Theorem Declaration |
| %total | | 9.3 Totality |
| %use | | 6.1 Installing an Extension |
| %worlds | | 9.1 Regular Worlds |
|
A | | |
| abbreviations | | 3.3 Definitions |
| add-hook | | 13.14 Emacs Initialization |
| ambiguity | | 4.5 Type Ascription |
| arguments, implicit | | 4.2 Implicit Arguments |
| arguments, mutual | | 8.6 Mutual Recursion |
| arithmetic | | 15 Examples |
| assumptions | | 5.5 Operational Semantics |
| auto-mode-alist | | 13.14 Emacs Initialization |
| autoload | | 13.14 Emacs Initialization |
|
B | | |
| backquote, before variables | | 2.2 Identifiers |
| bool | | 12.1 Server Types |
| bound variables | | 3.2 Constructor Declaration |
| breakpoints, from Emacs | | 13.5 Tracing Commands |
|
C | | |
| call patterns | | 8.1 Termination Declaration |
| Cartesian-closed categories | | 15 Examples |
| case, upper and lower | | 2.2 Identifiers |
| characters, reserved | | 2.1 Reserved Characters |
| Church-Rosser theorem | | 15 Examples |
| clause selection | | 5.5 Operational Semantics |
| colors | | 13.13 Syntax Highlighting |
| commands, Emacs | | 13.15 Command Summary |
| commands, server | | 12.2 Server Commands |
| Config.append | | 12.2 Server Commands |
| Config.load | | 12.2 Server Commands |
| Config.read | | 12.2 Server Commands |
| Configurations | | 11.1 Configurations |
| constraint domains | | 6 Constraint Domains |
| constraints | | 6 Constraint Domains |
| context, regular | | 10.1 Theorem Declaration |
| coverage | | 9 Coverage |
| current declaration | | 13.1 Twelf Mode |
| cut elimination | | 15 Examples |
|
D | | |
| decl | | 12.2 Server Commands |
| declaration | | 3.1 Grammar |
| declaration, current | | 13.1 Twelf Mode |
| declarations | | 3.1 Grammar |
| declarations, mode | | 7.1 Short Mode Declaration |
| declarations, name preference | | 3.5 Name Preferences |
| declarations, operator | | 3.4 Operator Declaration |
| declarations, reduction | | 8.2 Reduction Declaration |
| declarations, termination | | 8.1 Termination Declaration |
| declarations, theorem | | 10.1 Theorem Declaration |
| definitions | | 3.3 Definitions |
| definitions, family-level | | 5.7 Clause Definitions |
| definitions, in proof search | | 5.7 Clause Definitions |
| definitions, strict | | 4.4 Strict Definitions |
| definitions, type-level | | 5.7 Clause Definitions |
| display, of server buffer | | 13.3 Type Checking Commands |
| documentation | | 13.8 Info File |
|
E | | |
| editing | | 13.2 Editing Commands |
| Emacs variables | | 13.12 Emacs Variables |
| environment parameters | | 11.3 Environment Parameters |
| error messages | | 4.6 Error Messages |
| error tracking | | 13.6 Error Tracking |
| examples, from user’s guide | | 15 Examples |
| executing proofs | | 10.5 Proof Realizations |
| existential quantifier | | 10.1 Theorem Declaration |
|
F | | |
| faces | | 13.13 Syntax Highlighting |
| family-level definitions | | 5.7 Clause Definitions |
| file | | 12.1 Server Types |
| file names | | 1 Introduction |
| files, configuration | | 11.1 Configurations |
| files, loading | | 11.2 Loading Files |
| filling | | 10.3 Proof Steps |
| first-order logic | | 15 Examples |
| free variables | | 3.2 Constructor Declaration |
| freezing families | | 9.4 Subordination |
|
G | | |
| get | | 12.2 Server Commands |
|
H | | |
| help | | 12.2 Server Commands |
| Hilbert calculus | | 15 Examples |
| Horn logic, theory | | 15 Examples |
|
I | | |
| id | | 12.1 Server Types |
| identifiers, reserved | | 2.2 Identifiers |
| implicit arguments | | 4.2 Implicit Arguments |
| implicit quantifiers | | 4.1 Implicit Quantifiers |
| indentation | | 13.2 Editing Commands |
| info file | | 13.8 Info File |
| initializing Twelf mode | | 13.14 Emacs Initialization |
| input coverage | | 9.2 Input Coverage |
| input mode | | 7 Modes |
| installation | | 14 Installation |
| interrupt | | 13.7 Server State |
|