print_tac : string -> tactic
STRUCTURE
SYNOPSIS
Prints the goal; does not change it.
DESCRIPTION
The tactic print_tac s prints the string s followed by (the pretty-printed string of) the goal to which it is applied (using the standard SML print function). The effect on the goal is as if the tactic ALL_TAC had been applied (i.e., the state of the goal is not changed).
FAILURE
Never fails.
COMMENTS
This is useful for debugging tactic applications in contexts where the usual interactive goal-stack is not available.
SEEALSO
HOL  Kananaskis-14