TURNSTILE-INDENT : FLAG

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

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage