FLAG : flag or parameter

Top Levels

• 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

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

Vpforms

• lit-name
• order-components
• print-lit-name

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

Miscellaneous

• rewrite-equivs

RuleP

• rulep-mainfn
• rulep-wffeq

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

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

ETPS documentation homepage

TPS homepage