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