FLAG : flag or parameter

Top Levels

• mt-dups-per-quant
• proofw-active
• proofw-active+nos
• proofw-active+nos-height
• proofw-active+nos-width
• proofw-active-height
• proofw-active-width
• proofw-all
• proofw-all-height
• proofw-all-width

Style

• style

Review

• alpha-lower-flag
• last-mode-name

Modes

• suppress-flags
• suppress-flags-list

Help

• show-all-packages

Starting and Finishing

• completion-options
• history-size

OTL Object

• auto-generate-hyps
• cleanup-rulec
• cleanup-same
• default-wffeq
• print-dots
• printlineflag
• short-help

Printing

• print-combined-egens
• print-combined-ugens
• print-combined-uis
• print-until-ui-or-egen

Printing

• allscopeflag
• atomvalflag
• blank-lines-inserted
• charsize
• displaywff
• elim-defns
• fillineflag
• first-order-print-mode
• flushleftflag
• leftmargin
• localleftflag
• ppwfflag
• printdepth
• printtypes
• printtypes-all
• retain-initial-type
• rightmargin
• scope
• slides-preamble
• use-dot
• use-internal-print-mode

Internal for Printing

• infix-notation

TeX

• in-tex-math-mode
• latex-emulation
• pagelength
• tex-mimic-scribe

X Windows

• use-window-style
• window-style

Weak Labels

• print-weak

Flavors of Labels

• make-wffops-labels
• meta-label-name
• print-meta

Saving Work

• save-interval
• save-work-on-start-up
• save-work-p

Recording

• printedtfile
• printedtflag
• printedtflag-slides
• printedtops
• printmatefile
• printmateflag
• printmateflag-slides
• printmateops

Printing Proofs into Files

• latex-postamble
• latex-preamble
• scribe-line-width
• scribe-postamble
• scribe-preamble
• tex-1-postamble
• tex-1-preamble
• tex-line-width
• tex-postamble
• tex-preamble
• tpstex
• vpdtex

Proof Outline

• print-comments
• slides-turnstile-indent
• slides-turnstyle-indent
• support-numbers
• turnstile-indent
• turnstile-indent-auto
• turnstyle-indent
• turnstyle-indent-auto

Expansion Trees

• add-truth
• duplication-strategy
• duplication-strategy-pfd
• econj-name
• edisj-name
• empty-dup-info-name
• eproof-name
• expansion-name
• false-name
• imp-name
• initial-bktrack-limit
• leaf-name
• mating-name
• matingstree-name
• min-quantifier-scope
• neg-name
• print-deep
• print-nodenames
• renumber-leaves
• rewrite-defns
• rewrite-name
• selection-name
• show-skolem
• skolem-default
• skolem-selection-name
• true-name
• truthvalues-hack

Mtree Operations

• default-ob
• mt-default-ob-mate

Mtree Auto

• mt-subsumption-check
• mt94-12-trigger
• mtree-filter-dups
• mtree-stop-immediately
• tag-conn-fn
• tag-mating-fn

Mating search

• default-expand
• default-mate
• default-ms
• interrupt-enable
• mating-verbose
• monitorflag
• new-mating-after-dup
• query-user
• rec-ms-file
• rec-ms-filename
• use-diy
• use-fast-prop-search

MS88 search procedure

• added-conn-enabled
• considered-conn-enabled
• dup-allowed
• dupe-enabled
• dupe-var-enabled
• excluding-gc-time
• first-order-mode-ms
• incomp-mating-enabled
• mate-ffpair
• mate-subsumed-test-enabled
• mate-subsumed-true-enabled
• mating-changed-enabled
• ms-init-path
• ms-split
• occurs-check
• prim-quantifier
• primsub-enabled
• prop-strategy
• removed-conn-enabled
• search-complete-paths
• start-time-enabled
• stop-time-enabled
• timing-named
• unif-subsumed-test-enabled
• unif-subsumed-true-enabled

MS89 search procedure

• max-search-limit
• rank-eproof-fn
• search-time-limit

MS90-3 search procedure

• max-mates
• min-quant-etree
• ms90-3-dup-strategy
• num-frpairs
• print-mating-counter
• show-time

MS91-6 and MS91-7 search procedures

• ms91-interleave
• ms91-prefer-smaller
• ms91-time-by-vpaths
• ms91-weight-limit-range
• new-option-set-limit
• options-generate-arg
• options-generate-fn
• options-generate-update
• options-verbose
• penalty-for-each-primsub
• penalty-for-multiple-primsubs
• penalty-for-multiple-subs
• penalty-for-ordinary-dup
• reconsider-fn
• weight-a-coefficient
• weight-a-fn
• weight-b-coefficient
• weight-b-fn
• weight-c-coefficient
• weight-c-fn

MS98-1 search procedure

• break-at-quantifiers
• ff-delay
• hpath-threshold
• maximize-first
• ms98-base-prim
• ms98-dup-below-primsubs
• ms98-dup-primsubs
• ms98-first-fragment
• ms98-force-h-o
• ms98-fragment-order
• ms98-init
• ms98-low-memory
• ms98-max-components
• ms98-max-prims
• ms98-measure
• ms98-merge-dags
• ms98-minimality-check
• ms98-num-of-dups
• ms98-primsub-count
• ms98-rew-primsubs
• ms98-rewrite-depth
• ms98-rewrite-model
• ms98-rewrite-prune
• ms98-rewrite-size
• ms98-rewrite-unif
• ms98-rewrites
• ms98-unif-hack
• ms98-unif-hack2
• ms98-valid-pair
• ms98-variable-order
• ms98-verbose

Proof Translation

• etree-nat-verbose
• merge-minimize-mating
• natree-debug
• remove-leibniz

Unification

• apply-match
• countsubs-first
• dneg-imitation
• eta-rule
• imitation-first
• leibniz-sub-check
• max-dup-paths
• max-search-depth
• max-utree-depth
• min-quick-depth
• ms-dir
• ms90-3-quick
• pruning
• reduce-double-neg
• rigid-path-ck
• stop-at-tsn
• subsumption-check
• subsumption-depth
• subsumption-nodes
• total-num-of-dups
• uni-search-heuristic
• unif-counter
• unif-counter-output
• unif-trigger
• unify-verbose

Tactics

• default-tactic
• tacmode
• tactic-verbose
• tacuse

suggestions

• go-instructions
• quietly-use-defaults
• resolve-conflict

Searchlists

• test-easier-if-high
• test-easier-if-low
• test-easier-if-nil
• test-easier-if-t
• test-faster-if-high
• test-faster-if-low
• test-faster-if-nil
• test-faster-if-t
• test-fix-unif-depths
• test-increase-time
• test-initial-time-limit
• test-max-search-values
• test-next-search-fn
• test-reduce-time
• test-verbose
• testwin-height
• testwin-width

Vpforms

• lit-name
• order-components
• print-lit-name
• printvpdflag
• texformat
• vpd-brief
• vpd-filename
• vpd-lit-name
• vpd-ptypes
• vpd-style
• vpd-vpfpage
• vpform-labels
• vpform-tex-magnification
• vpform-tex-nest
• vpform-tex-preamble
• vpw-height
• vpw-width

Wff Editor

• edppwfflag
• edprintdepth
• edwin-current
• edwin-current-height
• edwin-current-width
• edwin-top
• edwin-top-height
• edwin-top-width
• edwin-vpform
• edwin-vpform-height
• edwin-vpform-width

wff Primitives

• meta-bdvar-name
• meta-var-name
• ren-var-fn
• rename-all-bd-vars

Wff Parsing

• base-type
• first-order-mode-parse
• lowercaseraise
• type-iota-mode
• untyped-lambda-calculus

Basic Abbreviations

• rewrite-equalities

Lambda-Calculus

• lambda-conv

Primitive Substitutions

• max-prim-depth
• max-prim-lits
• min-prim-depth
• min-prim-lits
• neg-prim-sub
• pr97c-max-abbrevs
• pr97c-prenex
• prim-bdtypes
• prim-bdtypes-auto
• prim-prefix
• primsub-method

Miscellaneous

• rewrite-equivs

RuleP

• rulep-mainfn
• rulep-wffeq

Skolemizing

• name-skolem-fn

Quantifiers

• ui-herbrand-limit

Auxiliary

• use-rulep
• use-symsimp

Events

• advice-asked-enabled
• advice-file
• command-enabled
• command-file
• done-exc-enabled
• error-enabled
• error-file
• event-cycle
• events-enabled
• input-error-enabled
• input-error-file
• proof-action-enabled
• proof-file
• quiet-events
• rule-error-enabled
• rule-error-file
• score-file

Grader

• cal-percentage
• course-name
• default-penalty-fn
• drop-min
• due-date-flag
• etps-file
• grade-dir
• grade-file
• letter-grade-file
• letter-grade-flag
• new-item
• old-grade-file
• old-totals-grade-file
• patch-file
• print-n-digits
• statistical-options
• totals-grade-file

Maintenance

• compiled-extension
• expertflag
• init-dialogue
• init-dialogue-fn
• lisp-implementation-type
• load-warn-p
• machine-instance
• machine-type
• news-dir
• read-lload-sources-p
• save-file
• short-site-name
• source-extension
• source-path
• test-modify
• test-theorems

Rules object

• build-match
• hline-justification
• treat-hlines-as-dlines

Unclassified

• max-substs-proj
• max-substs-proj-total
• max-substs-quick
• max-substs-var
• num-of-dups
• primsub-var-select

Library

• add-subdirectories
• backup-lib-dir
• default-lib-dir
• default-libfile-type
• default-libindex-type
• lib-bestmode-file
• lib-keyword-file
• lib-masterindex-file
• recordflags
• remove-trailing-dir
• show-all-libobjects

Bugs

• default-bug-dir
• use-default-bug-dir

TPS documentation homepage

TPS homepage