----------------------------------------------------------------------
print_tac                                                  (goalStack)
----------------------------------------------------------------------
print_tac : string -> tactic

SYNOPSIS
Prints the goal; does not change it.

KEYWORDS
goalstack

DESCRIBE
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
Tactical.ALL_TAC.

----------------------------------------------------------------------