TURNSTYLE-INDENT : FLAG

TURNSTYLE-INDENT is a flag or parameter.
Number of columns (from leftmargin) that turnstile should be
indented when writing proofs in a SCRIBE file or on the screen. Notice
that slides use a different flag, SLIDES-TURNSTYLE-INDENT.
This flag and TURNSTILE-INDENT are synonymous.
TURNSTYLE-INDENT takes values of type INTEGER+.
It belongs to subjects PRINTING OTL-VARS .
Its default value is 13
Its current value is 13.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage