| Index Entry | | Section |
|
P | | |
| parameter block | | 9.1 Regular Worlds |
| parameters | | 5.5 Operational Semantics |
| parameters, environment | | 11.3 Environment Parameters |
| Poly/ML | | 14 Installation |
| precedence | | 3.4 Operator Declaration |
| Print.domains | | 12.2 Server Commands |
| Print.prog | | 12.2 Server Commands |
| Print.prog | | 12.2 Server Commands |
| Print.sgn | | 12.2 Server Commands |
| Print.sgn | | 12.2 Server Commands |
| Print.subord | | 12.2 Server Commands |
| printing, from Emacs | | 13.4 Printing Commands |
| printing, signature | | 11.4 Signature Printing |
| proof realizations | | 10.5 Proof Realizations |
|
Q | | |
| quantifier, existential | | 10.1 Theorem Declaration |
| quantifier, universal | | 10.1 Theorem Declaration |
| quantifiers, implicit | | 4.1 Implicit Quantifiers |
| queries | | 5.1 Query Declaration |
| queries, interactive | | 5.3 Interactive Queries |
| quit | | 12.2 Server Commands |
|
R | | |
| reconTraceMode | | 12.1 Server Types |
| recursion | | 10.3 Proof Steps |
| reduction declarations | | 8.2 Reduction Declaration |
| reduction predicate | | 8.2 Reduction Declaration |
| regular context | | 9.1 Regular Worlds |
| regular context | | 10.1 Theorem Declaration |
| regular worlds | | 9.1 Regular Worlds |
| reserved characters | | 2.1 Reserved Characters |
| reserved identifiers | | 2.2 Identifiers |
| reset | | 12.2 Server Commands |
| right | | 3.4 Operator Declaration |
| rigid occurrences | | 4.3 Strict Occurrences |
| running time | | 11.6 Timing Statistics |
|
S | | |
| search strategy | | 10.4 Search Strategies |
| semantics, operational | | 5.5 Operational Semantics |
| server | | 12 Twelf Server |
| server buffer | | 13.3 Type Checking Commands |
| server commands | | 12.2 Server Commands |
| server parameters, setting | | 13.7 Server State |
| server state | | 13.7 Server State |
| server timers | | 13.10 Twelf Timers |
| server types | | 12.1 Server Types |
| set | | 12.2 Server Commands |
| setting server parameters | | 13.7 Server State |
| signature | | 3.1 Grammar |
| signature printing | | 11.4 Signature Printing |
| signature TWELF | | 11.7 Twelf Signature |
| solving queries | | 5.2 Solve Declaration |
| splitting | | 10.3 Proof Steps |
| Standard ML of New Jersey | | 14 Installation |
| statistics | | 11.6 Timing Statistics |
| strategy | | 12.1 Server Types |
| strict definitions | | 4.4 Strict Definitions |
| strict occurrences | | 4.3 Strict Occurrences |
| structure Twelf | | 11.7 Twelf Signature |
| subgoal selection | | 5.5 Operational Semantics |
| subordination | | 9.4 Subordination |
| subterm order | | 8.3 Subterm Ordering |
| syntax highlighting | | 13.13 Syntax Highlighting |
|
T | | |
| Table.top | | 12.2 Server Commands |
| tabled logic programming | | 5.9 Tabled Logic Programming |
| tableStrategy | | 12.1 Server Types |
| tagging configurations | | 13.9 Tags Files |
| tags file | | 13.9 Tags Files |
| term | | 3.1 Grammar |
| term reconstruction | | 4 Term Reconstruction |
| termination checking | | 8 Termination |
| termination declarations | | 8.1 Termination Declaration |
| termination order | | 8.1 Termination Declaration |
| TeX output | | 11.4 Signature Printing |
| theorem declarations | | 10.1 Theorem Declaration |
| theorem prover | | 10 Theorem Prover |
| Timers.check | | 12.2 Server Commands |
| Timers.reset | | 12.2 Server Commands |
| Timers.show | | 12.2 Server Commands |
| timing statistics | | 11.6 Timing Statistics |
| top | | 12.2 Server Commands |
| top-level, query | | 5.3 Interactive Queries |
| totality | | 9.3 Totality |
| Trace.break | | 12.2 Server Commands |
| Trace.breakAll | | 12.2 Server Commands |
| Trace.detail | | 11.5 Tracing and Breakpoints |
| Trace.reset | | 12.2 Server Commands |
| Trace.show | | 12.2 Server Commands |
| Trace.trace | | 12.2 Server Commands |
| Trace.traceAll | | 12.2 Server Commands |
| Trace.unbreak | | 12.2 Server Commands |
| Trace.untrace | | 12.2 Server Commands |
| tracing reconstruction | | 4.7 Tracing Reconstruction |
| tracing, from Emacs | | 13.5 Tracing Commands |
| tracking errors | | 13.6 Error Tracking |
| Twelf home page | | 1 Introduction |
| Twelf mode in Emacs | | 13.1 Twelf Mode |
| Twelf server | | 12 Twelf Server |
| twelf-indent | | 13.12 Emacs Variables |
| twelf-info-file | | 13.12 Emacs Variables |
| twelf-mode-hook | | 13.12 Emacs Variables |
| twelf-server-mode-hook | | 13.12 Emacs Variables |
| twelf-server-program | | 13.12 Emacs Variables |
| Twelf-SML mode | | 13.11 Twelf-SML Mode |
| twelf-sml-mode-hook | | 13.12 Emacs Variables |
| twelf-sml-program | | 13.12 Emacs Variables |
| Twelf.ABORT | | 11.1 Configurations |
| Twelf.chatter | | 11.3 Environment Parameters |
| Twelf.Compile.optimize | | 5.5 Operational Semantics |
| Twelf.Compile.optimize | | 11.3 Environment Parameters |
| Twelf.Config.append | | 11.1 Configurations |
| Twelf.Config.define | | 11.1 Configurations |
| Twelf.Config.load | | 11.1 Configurations |
| Twelf.Config.read | | 11.1 Configurations |
| Twelf.Config.suffix | | 11.1 Configurations |
| Twelf.doubleCheck | | 11.3 Environment Parameters |
| Twelf.loadFile | | 11.2 Loading Files |
| Twelf.make | | 11.1 Configurations |
| Twelf.OK | | 11.1 Configurations |
| Twelf.OS.chDir | | 11.1 Configurations |
| Twelf.OS.getDir | | 11.1 Configurations |
| Twelf.Print.depth | | 11.3 Environment Parameters |
| Twelf.Print.implicit | | 4.7 Tracing Reconstruction |
| Twelf.Print.implicit | | 11.3 Environment Parameters |
| Twelf.Print.indent | | 11.3 Environment Parameters |
| Twelf.Print.length | | 11.3 Environment Parameters |
| Twelf.Print.prog | | 11.4 Signature Printing |
| Twelf.Print.sgn | | 11.4 Signature Printing |
| Twelf.Print.subord | | 9.4 Subordination |
| Twelf.Print.TeX.prog | | 11.4 Signature Printing |
| Twelf.Print.TeX.sgn | | 11.4 Signature Printing |
| Twelf.Print.width | | 11.3 Environment Parameters |
| Twelf.Prover.FRS | | 10.4 Search Strategies |
| Twelf.Prover.maxRecurse | | 10.3 Proof Steps |
| Twelf.Prover.maxRecurse | | 11.3 Environment Parameters |
| Twelf.Prover.maxSplit | | 10.3 Proof Steps |
| Twelf.Prover.maxSplit | | 11.3 Environment Parameters |
| Twelf.Prover.RFS | | 10.4 Search Strategies |
| Twelf.Prover.strategy | | 10.4 Search Strategies |
| Twelf.Prover.strategy | | 11.3 Environment Parameters |
| Twelf.Recon.Omiscient | | 4.7 Tracing Reconstruction |
| Twelf.Recon.Progressive | | 4.7 Tracing Reconstruction |
| Twelf.Recon.trace | | 4.7 Tracing Reconstruction |
| Twelf.Recon.traceMode | | 4.7 Tracing Reconstruction |
| Twelf.Recon.TraceMode | | 4.7 Tracing Reconstruction |
| Twelf.reset | | 11.2 Loading Files |
| Twelf.Table.strategy | | 5.9 Tabled Logic Programming |
| Twelf.Table.strategy | | 11.3 Environment Parameters |
| Twelf.Table.strengthen | | 5.9 Tabled Logic Programming |
| Twelf.Table.strengthen | | 11.3 Environment Parameters |
| Twelf.Table.Subsumption | | 5.9 Tabled Logic Programming |
| Twelf.Table.top | | 5.9 Tabled Logic Programming |
| Twelf.Table.Variant | | 5.9 Tabled Logic Programming |
| Twelf.Timers.check | | 11.6 Timing Statistics |
| Twelf.Timers.reset | | 11.6 Timing Statistics |
| Twelf.Timers.show | | 11.6 Timing Statistics |
| Twelf.Trace.All | | 11.5 Tracing and Breakpoints |
| Twelf.Trace.break | | 11.5 Tracing and Breakpoints |
| Twelf.Trace.detail | | 11.3 Environment Parameters |
| Twelf.Trace.None | | 11.5 Tracing and Breakpoints |
| Twelf.Trace.reset | | 11.5 Tracing and Breakpoints |
| Twelf.Trace.show | | 11.5 Tracing and Breakpoints |
| Twelf.Trace.Some | | 11.5 Tracing and Breakpoints |
| Twelf.Trace.trace | | 11.5 Tracing and Breakpoints |
| Twelf.unsafe | | 10.1 Theorem Declaration |
| Twelf.unsafe | | 11.3 Environment Parameters |
| type ascription | | 4.5 Type Ascription |
| type checking, from Emacs | | 13.3 Type Checking Commands |
| type families | | 3 Syntax |
| type inference example | | 5.6 Sample Program |
| type reconstruction | | 4 Term Reconstruction |
| type-level definitions | | 5.7 Clause Definitions |
| types | | 3 Syntax |
| types, server | | 12.1 Server Types |
| typographical conventions | | 1 Introduction |
|