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 subtermPrint hypotheses and the current subterm. The printing of hypotheses (and perhaps governors) are controlled as in the
General Form: (th &optional hyps-indices govs-indices)
hypscommand; see its documentation.
Historical note: The name
th is adapted from the Gypsy Verification
th abbreviates the command
says to print information on the current goal.