| Index Entry | Section |
|---|
|
| P | | |
|---|
| parameter block | 10.1 Regular Worlds |
| parameters | 6.5 Operational Semantics |
| parameters, environment | 12.3 Environment Parameters |
| Poly/ML | 15. Installation |
| precedence | 3.4 Operator Declaration |
| Print.domains | 13.2 Server Commands |
| Print.prog | 13.2 Server Commands |
| Print.prog | 13.2 Server Commands |
| Print.sgn | 13.2 Server Commands |
| Print.sgn | 13.2 Server Commands |
| Print.subord | 13.2 Server Commands |
| printing, from Emacs | 14.4 Printing Commands |
| printing, signature | 12.4 Signature Printing |
| proof realizations | 11.5 Proof Realizations |
|
| Q | | |
|---|
| quantifier, existential | 11.1 Theorem Declaration |
| quantifier, universal | 11.1 Theorem Declaration |
| quantifiers, implicit | 4.1 Implicit Quantifiers |
| queries | 6.1 Query Declaration |
| queries, interactive | 6.3 Interactive Queries |
| quit | 13.2 Server Commands |
|
| R | | |
|---|
| reconTraceMode | 13.1 Server Types |
| recursion | 11.3 Proof Steps |
| reduction declarations | 9.2 Reduction Declaration |
| reduction predicate | 9.2 Reduction Declaration |
| regular context | 10.1 Regular Worlds |
| regular context | 11.1 Theorem Declaration |
| regular worlds | 10.1 Regular Worlds |
| reserved characters | 2.1 Reserved Characters |
| reserved identifiers | 2.2 Identifiers |
| reset | 13.2 Server Commands |
| right | 3.4 Operator Declaration |
| rigid occurrences | 4.3 Strict Occurrences |
| running time | 12.6 Timing Statistics |
|
| S | | |
|---|
| search strategy | 11.4 Search Strategies |
| semantics, operational | 6.5 Operational Semantics |
| server | 13. Twelf Server |
| server buffer | 14.3 Type Checking Commands |
| server commands | 13.2 Server Commands |
| server parameters, setting | 14.7 Server State |
| server state | 14.7 Server State |
| server timers | 14.10 Twelf Timers |
| server types | 13.1 Server Types |
| set | 13.2 Server Commands |
| setting server parameters | 14.7 Server State |
| signature | 3.1 Grammar |
| signature | 5.1 Signature Declaration |
| signature printing | 12.4 Signature Printing |
| signature TWELF | 12.7 Twelf Signature |
| solving queries | 6.2 Solve Declaration |
| splitting | 11.3 Proof Steps |
| Standard ML of New Jersey | 15. Installation |
| statistics | 12.6 Timing Statistics |
| strategy | 13.1 Server Types |
| strict definitions | 4.4 Strict Definitions |
| strict occurrences | 4.3 Strict Occurrences |
| structure | 5.2 Structure Declaration |
| structure Twelf | 12.7 Twelf Signature |
| subgoal selection | 6.5 Operational Semantics |
| subordination | 10.4 Subordination |
| subterm order | 9.3 Subterm Ordering |
| syntax highlighting | 14.13 Syntax Highlighting |
|
| T | | |
|---|
| Table.top | 13.2 Server Commands |
| tabled logic programming | 6.9 Tabled Logic Programming |
| tableStrategy | 13.1 Server Types |
| tagging configurations | 14.9 Tags Files |
| tags file | 14.9 Tags Files |
| term | 3.1 Grammar |
| term reconstruction | 4. Term Reconstruction |
| termination checking | 9. Termination |
| termination declarations | 9.1 Termination Declaration |
| termination order | 9.1 Termination Declaration |
| TeX output | 12.4 Signature Printing |
| theorem declarations | 11.1 Theorem Declaration |
| theorem prover | 11. Theorem Prover |
| Timers.check | 13.2 Server Commands |
| Timers.reset | 13.2 Server Commands |
| Timers.show | 13.2 Server Commands |
| timing statistics | 12.6 Timing Statistics |
| top | 13.2 Server Commands |
| top-level, query | 6.3 Interactive Queries |
| totality | 10.3 Totality |
| Trace.break | 13.2 Server Commands |
| Trace.breakAll | 13.2 Server Commands |
| Trace.detail | 12.5 Tracing and Breakpoints |
| Trace.reset | 13.2 Server Commands |
| Trace.show | 13.2 Server Commands |
| Trace.trace | 13.2 Server Commands |
| Trace.traceAll | 13.2 Server Commands |
| Trace.unbreak | 13.2 Server Commands |
| Trace.untrace | 13.2 Server Commands |
| tracing reconstruction | 4.7 Tracing Reconstruction |
| tracing, from Emacs | 14.5 Tracing Commands |
| tracking errors | 14.6 Error Tracking |
| Twelf home page | 1. Introduction |
| Twelf mode in Emacs | 14.1 Twelf Mode |
| Twelf server | 13. Twelf Server |
| twelf-indent | 14.12 Emacs Variables |
| twelf-info-file | 14.12 Emacs Variables |
| twelf-mode-hook | 14.12 Emacs Variables |
| twelf-server-mode-hook | 14.12 Emacs Variables |
| twelf-server-program | 14.12 Emacs Variables |
| Twelf-SML mode | 14.11 Twelf-SML Mode |
| twelf-sml-mode-hook | 14.12 Emacs Variables |
| twelf-sml-program | 14.12 Emacs Variables |
| Twelf.ABORT | 12.1 Configurations |
| Twelf.chatter | 12.3 Environment Parameters |
| Twelf.Compile.optimize | 6.5 Operational Semantics |
| Twelf.Compile.optimize | 12.3 Environment Parameters |
| Twelf.Config.append | 12.1 Configurations |
| Twelf.Config.define | 12.1 Configurations |
| Twelf.Config.load | 12.1 Configurations |
| Twelf.Config.read | 12.1 Configurations |
| Twelf.Config.suffix | 12.1 Configurations |
| Twelf.doubleCheck | 12.3 Environment Parameters |
| Twelf.loadFile | 12.2 Loading Files |
| Twelf.make | 12.1 Configurations |
| Twelf.OK | 12.1 Configurations |
| Twelf.OS.chDir | 12.1 Configurations |
| Twelf.OS.getDir | 12.1 Configurations |
| Twelf.Print.depth | 12.3 Environment Parameters |
| Twelf.Print.implicit | 4.7 Tracing Reconstruction |
| Twelf.Print.implicit | 12.3 Environment Parameters |
| Twelf.Print.indent | 12.3 Environment Parameters |
| Twelf.Print.length | 12.3 Environment Parameters |
| Twelf.Print.prog | 12.4 Signature Printing |
| Twelf.Print.sgn | 12.4 Signature Printing |
| Twelf.Print.subord | 10.4 Subordination |
| Twelf.Print.TeX.prog | 12.4 Signature Printing |
| Twelf.Print.TeX.sgn | 12.4 Signature Printing |
| Twelf.Print.width | 12.3 Environment Parameters |
| Twelf.Prover.FRS | 11.4 Search Strategies |
| Twelf.Prover.maxRecurse | 11.3 Proof Steps |
| Twelf.Prover.maxRecurse | 12.3 Environment Parameters |
| Twelf.Prover.maxSplit | 11.3 Proof Steps |
| Twelf.Prover.maxSplit | 12.3 Environment Parameters |
| Twelf.Prover.RFS | 11.4 Search Strategies |
| Twelf.Prover.strategy | 11.4 Search Strategies |
| Twelf.Prover.strategy | 12.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 | 12.2 Loading Files |
| Twelf.Table.strategy | 6.9 Tabled Logic Programming |
| Twelf.Table.strategy | 12.3 Environment Parameters |
| Twelf.Table.strengthen | 6.9 Tabled Logic Programming |
| Twelf.Table.strengthen | 12.3 Environment Parameters |
| Twelf.Table.Subsumption | 6.9 Tabled Logic Programming |
| Twelf.Table.top | 6.9 Tabled Logic Programming |
| Twelf.Table.Variant | 6.9 Tabled Logic Programming |
| Twelf.Timers.check | 12.6 Timing Statistics |
| Twelf.Timers.reset | 12.6 Timing Statistics |
| Twelf.Timers.show | 12.6 Timing Statistics |
| Twelf.Trace.All | 12.5 Tracing and Breakpoints |
| Twelf.Trace.break | 12.5 Tracing and Breakpoints |
| Twelf.Trace.detail | 12.3 Environment Parameters |
| Twelf.Trace.None | 12.5 Tracing and Breakpoints |
| Twelf.Trace.reset | 12.5 Tracing and Breakpoints |
| Twelf.Trace.show | 12.5 Tracing and Breakpoints |
| Twelf.Trace.Some | 12.5 Tracing and Breakpoints |
| Twelf.Trace.trace | 12.5 Tracing and Breakpoints |
| Twelf.unsafe | 11.1 Theorem Declaration |
| Twelf.unsafe | 12.3 Environment Parameters |
| type ascription | 4.5 Type Ascription |
| type checking, from Emacs | 14.3 Type Checking Commands |
| type families | 3. Syntax |
| type inference example | 6.6 Sample Program |
| type reconstruction | 4. Term Reconstruction |
| type-level definitions | 6.7 Clause Definitions |
| types | 3. Syntax |
| types, server | 13.1 Server Types |
| typographical conventions | 1. Introduction |
|