| Index Entry | | Section |
|
K | | |
| kinds | | 3 Syntax |
| Kolmogorov translation | | 15 Examples |
|
L | | |
| lambda calculus example | | 5.6 Sample Program |
| lambda-calculus, polymorphic | | 15 Examples |
| lambda-calculus, untyped | | 15 Examples |
| left | | 3.4 Operator Declaration |
| LF | | 1 Introduction |
| limit | | 12.1 Server Types |
| load-path | | 13.14 Emacs Initialization |
| loadFile | | 12.2 Server Commands |
| loading files | | 11.2 Loading Files |
| local assumptions | | 5.5 Operational Semantics |
| local parameters | | 5.5 Operational Semantics |
| logic programming | | 5 Logic Programming |
| logic programming, theory | | 15 Examples |
| logical framework | | 1 Introduction |
|
M | | |
| M-x backward-delete-char-untabify | | 13.2 Editing Commands |
| M-x find-tag | | 13.9 Tags Files |
| M-x find-tag-other-window | | 13.9 Tags Files |
| M-x tags-loop-continue | | 13.9 Tags Files |
| M-x tags-query-replace | | 13.9 Tags Files |
| M-x tags-search | | 13.9 Tags Files |
| M-x twelf-check-declaration | | 13.3 Type Checking Commands |
| M-x twelf-font-fontify-buffer | | 13.13 Syntax Highlighting |
| M-x twelf-font-fontify-decl | | 13.13 Syntax Highlighting |
| M-x twelf-font-unfontify | | 13.13 Syntax Highlighting |
| M-x twelf-get | | 13.7 Server State |
| M-x twelf-goto-error | | 13.6 Error Tracking |
| M-x twelf-indent-decl | | 13.2 Editing Commands |
| M-x twelf-indent-line | | 13.2 Editing Commands |
| M-x twelf-indent-region | | 13.2 Editing Commands |
| M-x twelf-info | | 13.8 Info File |
| M-x twelf-mode | | 13.1 Twelf Mode |
| M-x twelf-next-error | | 13.6 Error Tracking |
| M-x twelf-print-program | | 13.4 Printing Commands |
| M-x twelf-print-signature | | 13.4 Printing Commands |
| M-x twelf-print-subord | | 13.4 Printing Commands |
| M-x twelf-print-tex-program | | 13.4 Printing Commands |
| M-x twelf-print-tex-signature | | 13.4 Printing Commands |
| M-x twelf-reset | | 13.7 Server State |
| M-x twelf-save-append-config | | 13.3 Type Checking Commands |
| M-x twelf-save-check-config | | 13.3 Type Checking Commands |
| M-x twelf-save-check-file | | 13.3 Type Checking Commands |
| M-x twelf-server | | 13.7 Server State |
| M-x twelf-server-configure | | 13.7 Server State |
| M-x twelf-server-display | | 13.3 Type Checking Commands |
| M-x twelf-server-interrupt | | 13.7 Server State |
| M-x twelf-server-quit | | 13.7 Server State |
| M-x twelf-server-restart | | 13.7 Server State |
| M-x twelf-server-send-command | | 13.7 Server State |
| M-x twelf-set | | 13.7 Server State |
| M-x twelf-sml | | 13.11 Twelf-SML Mode |
| M-x twelf-sml-cd | | 13.11 Twelf-SML Mode |
| M-x twelf-sml-quit | | 13.11 Twelf-SML Mode |
| M-x twelf-sml-send-newline | | 13.11 Twelf-SML Mode |
| M-x twelf-sml-send-query | | 13.11 Twelf-SML Mode |
| M-x twelf-sml-send-region | | 13.11 Twelf-SML Mode |
| M-x twelf-sml-send-semicolon | | 13.11 Twelf-SML Mode |
| M-x twelf-tag | | 13.9 Tags Files |
| M-x twelf-timers-check | | 13.10 Twelf Timers |
| M-x twelf-timers-reset | | 13.10 Twelf Timers |
| M-x twelf-timers-show | | 13.10 Twelf Timers |
| M-x twelf-to-twelf-sml-mode | | 13.11 Twelf-SML Mode |
| M-x twelf-trace-break | | 13.5 Tracing Commands |
| M-x twelf-trace-break-all | | 13.5 Tracing Commands |
| M-x twelf-trace-show | | 13.5 Tracing Commands |
| M-x twelf-trace-trace | | 13.5 Tracing Commands |
| M-x twelf-trace-trace-all | | 13.5 Tracing Commands |
| M-x twelf-trace-unbreak | | 13.5 Tracing Commands |
| M-x twelf-trace-untrace | | 13.5 Tracing Commands |
| M-x twelf-type-const | | 13.3 Type Checking Commands |
| make | | 12.2 Server Commands |
| meta-logic | | 10 Theorem Prover |
| meta-theorem verification | | 9 Coverage |
| meta-theorem verification | | 9.3 Totality |
| Mini-ML, compilation | | 15 Examples |
| Mini-ML, theory | | 15 Examples |
| Mini-ML, with units | | 15 Examples |
| ML implementations | | 14 Installation |
| ML interface | | 11 ML Interface |
| MLton | | 14 Installation |
| mode checking | | 7.3 Mode Checking |
| mode declaration, full form | | 7.2 Full Mode Declaration |
| mode declarations, short form | | 7.1 Short Mode Declaration |
| modes | | 7 Modes |
| mutual arguments | | 8.6 Mutual Recursion |
| mutual recursion | | 8.6 Mutual Recursion |
|
N | | |
| name preferences | | 3.5 Name Preferences |
| nat | | 12.1 Server Types |
| natural deduction | | 3.6 Sample Signature |
| none | | 3.4 Operator Declaration |
| numbers | | 6 Constraint Domains |
|
O | | |
| objects | | 3 Syntax |
| occurrences, rigid | | 4.3 Strict Occurrences |
| occurrences, strict | | 4.3 Strict Occurrences |
| open | | 11 ML Interface |
| operational semantics | | 5.5 Operational Semantics |
| operator declarations | | 3.4 Operator Declaration |
| order | | 8.1 Termination Declaration |
| order, lexicographic | | 8.4 Lexicographic Orders |
| order, simultaneous | | 8.5 Simultaneous Orders |
| order, subterm | | 8.3 Subterm Ordering |
| ordered logic | | 15 Examples |
| OS.chDir | | 12.2 Server Commands |
| OS.exit | | 12.2 Server Commands |
| OS.getDir | | 12.2 Server Commands |
| output coverage | | 9.3 Totality |
| output mode | | 7 Modes |
|