INFO : flag setting or other piece of information

Top Levels

• command-line-switches

Collecting Help

• econj*
• iconj*
• loud
• quiet
• test-bool
• test-default
• test-long
• test-ms98
• test-short
• test-un88
• ugen*

Printing

• prfw-pall
• prfw-^p
• prfw-^pn

Proof Outline

• compress
• fix
• min
• vary

Expansion Trees

• dual
• dup-all
• dup-inner
• dup-outer
• eager
• lazy1
• lazy2

NIL

• none
• sk1
• sk3

Mtree Operations

• d-highest
• d-smallest
• deepest
• hi-lo
• highest
• lowest

Mtree Auto

• multiply-tag-list
• same-conns
• same-tag
• subset-conns
• tag-conn-leafno
• tag-conn-quick

Mating search

• ms98-1
• mtree
• mtree-1
• mtree-2
• npfd
• npfd-1
• oset
• otree
• pfd
• query-jforms
• query-slists
• show-jforms

MS88 search procedure

• allow-duplicates
• hash-table
• pushnew

MS89 search procedure

• num-vpaths-ranking

MS91-6 and MS91-7 search procedures

• add-options-count
• add-options-original
• add-options-subs
• add-options-weight
• all-penalties-fn
• double-arg
• double-weight
• expansion-level-weight-a
• ident-arg
• increment-weight
• inf-arg
• inf-weight
• option-set-num-leaves
• option-set-num-vpaths
• simple-weight-b-fn
• simplest-weight-b-fn
• square-arg
• square-weight

Unification

• all-nodes
• always
• apply-match-all-frdpairs
• apply-match-all-frdpairs-msv
• apply-match-max-substs
• apply-match-min-substs
• apply-match-most-consts
• best-first
• breadth-first
• const
• const-flex
• depth-first
• flex
• leaf-nodes
• never
• path-nodes
• quasi-tps1

Tactics

• auto
• etree-nat
• interactive
• mate-srch
• nat-ded

suggestions

• ask
• do
• forget
• show

Searchlists

• breadth-first-search
• exhaustive-search
• press-down
• press-down-2
• push-up
• push-up-2

wff Primitives

• ren-var-x1
• ren-var-x11
• ren-var-xa

Basic Abbreviations

• all
• leibniz
• only-ext

Lambda-Calculus

• beta-eta-only
• beta-eta-separate
• beta-eta-together

Primitive Substitutions

• append
• append-sub
• ignore
• pr89
• pr93
• pr95
• pr97
• pr97a
• pr97b
• pr97c
• replace
• replace-sub

Maintenance

• init-define-my-default-mode
• init-dialogue-default-fn

TPS documentation homepage

TPS homepage