REMARK_TAC : string -> tactic
- SYNOPSIS
-
A tactic version of remark.
- DESCRIPTION
-
Given any goal A ?- p, the tactic REMARK_TAC s prints the string s
to standard output.
As remark does, this outputs a string only if verbose flag is set.
- FAILURE CONDITIONS
-
Never fails.
- SEE ALSO
-
PRINT_GOAL_TAC, remark, verbose