th is adapted from the Gypsy Verification
Environment, where th abbreviates the command theorem, which
says to print information on the current goal.
print the top-level hypotheses and the current subterm
Major Section: PROOF-CHECKER-COMMANDS
Examples:
th -- print all (top-level) hypotheses and the current
subterm
(th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4,
and the current subterm
(th (1 3) t) -- print hypotheses 1 and 3 and all governors, and
the current subterm
General Form:
(th &optional hyps-indices govs-indices)
Print hypotheses and the current subterm. The printing of
hypotheses (and perhaps governors) are controlled as in the hyps
command; see its documentation.
Historical note: The name th is adapted from the Gypsy Verification
Environment, where th abbreviates the command theorem, which
says to print information on the current goal.