CONTEXT : context

Top Levels

• subtoplevels

Style

• style

Review

• flags

Flags

• flag-review

Modes

• flag-modes

Reading help

• rd-help

Help

• help-obj

Collecting Help

• coll-help

Concept

• concept-terminal

Starting and Finishing

• otl-entering

OTL Object

• otl-object

Printing

• otl-printing

Printing

• wff-printing

Internal for Printing

• print-internals

SAIL characters

• sail-chars

Script Letters

• script-letters

Subscripts

• subscripts

Superscripts

• superscripts

Lowercase Greek

• greek-letters-lowercase

Uppercase Greek

• greek-letters-uppercase

Greek Subscripts

• greek-subscripts

Bold Letters

• bold-letters

TeX

• tex-style

X Windows

• xwindows

Other Symbols

• misc-symbols

Weak Labels

• weak-labels

Flavors of Labels

• flavor-obj

Saving Work

• save-work-obj

Saving Wffs

• saving-wffs

Recording

• scribe-record

Printing Proofs into Files

• otl-files

Proof Outline

• proof-outline

Expansion Trees

• expansion-trees

Mtree Operations

• mtree-ops

Mtree Printing

• mtree-print

Mtree Auto

• mtree-auto

Search Suggestions

• search-suggestions

Mating search

• mating-search

MS88 search procedure

• ms88

MS89 search procedure

• ms89

MS90-3 search procedure

• ms90-3

MS90-9 search procedure

• ms90-9

MS91-6 and MS91-7 search procedures

• ms91

MS92-9 search procedure

• ms92-9

MS93-1 search procedure

• ms93-1

MS98-1 search procedure

• ms98-1

Proof Translation

• etr-nat

Unification

• unification

Dpairs

• unification-dpairs

Tactics

• tactics

suggestions

• suggestions

Searchlists

• test-searchlists

Library

• test-lib

Vpforms

• jforms1

Rearranging the Proof

• otl-rearranging

Status

• otl-status

Miscellaneous Rules

• rules-1-misc

Propositional Rules

• rules-2-prop

Negation Rules

• rules-3-neg

Quantifier Rules

• rules-4-quant

Substitution Rules

• rules-5-subst

Equality Rules

• rules-6-equality

Definition Rules

• rules-7-defn

Lambda Conversion Rules

• rules-8-lambda

Book Theorems

• book-theorems

Theorems

• tps-theorems

First-Order Logic

• ml1-exercises

Higher-Order Logic

• ml2-exercises

Wff Editor

• editor-obj

well-formed formula

• well-ff

wff Primitives

• prim-obj

Wff Parsing

• wff-parsing

Equality between Wffs

• wffequal

Predicates on Wffs

• wfftst-obj

Wff Types

• wfftyp-obj

Moving Commands

• moving

Changing Commands

• changing

Recursively Changing Commands

• recursively-changing

Embedding Commands

• embedding

Rewriting commands

• rewriting

Substitution

• substitution

Basic Abbreviations

• abbrev-ops

Set Abbreviations

• abbrev-set-ops

Lambda-Calculus

• lambda-op

Negation movers

• neg-ops

Primitive Substitutions

• primsubs

Miscellaneous

• misc-edops

RuleP

• rulep-test

Skolemizing

• skolems

Quantifier Commands

• develop-seqs

Wellformedness

• ill-formed

Compound

• compound-tactics

Propositional

• prop-tactics

Quantifiers

• quant-tactics

Equality

• equality-tactics

Definitions

• defn-tactics

Lambda

• lambda-tactics

Auxiliary

• aux-tactics

Events

• tps-events

report package

• report-object

File Utilities

• file-operations

Example of Report

• report-examples

Statistics

• stats

Grader

• grader-object

Getting Out and Help

• gr-a-out

Variables

• gr-b-vars

The Grade-File

• gr-c-gradefile

Manual Grades

• gr-d-manual-grades

Automatic Grades

• gr-e-automatic-grades

The Class List

• gr-f-class-list

Making the Output Convenient

• gr-g-output

Generating Values

• gr-h-stat

Displaying Information

• gr-i-display

Totaling

• gr-j-totals

Maintenance

• tps-maintenance

Sorting

• gr-k-sorting

Letter-Grades

• gr-l-letter-grade

Basics

• basics

Modules

• modules-in-tps

Rule Commands

• rule-commands

Rules Module

• rule-run

Lisp packages

• lisp-packages

Rules object

• rules-object

News

• system-news

Core Images

• core-image

Indirect Files

• indirect

Batch Control

• batch

Documentation

• documentation

Command declaration

• command-declaration

Lisp Source

• lisp-source

Miscellaneous

• miscellaneous

Unclassified

• unclassified

Library

• library

Display

• lib-display

Reading

• lib-reading

Editing

• lib-writing

Keywords

• lib-keys

Best modes

• lib-modes

Bugs

• lib-bugs

TPS documentation homepage

TPS homepage

CONTEXT : ARGTYPE

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage