NO_TAC : tactic
# g `T`;; val it : goalstack = 1 subgoal (1 total) `T` # e NO_TAC;; Exception: Failure "NO_TAC".
# e(REWRITE_TAC[] THEN NO_TAC);; val it : goalstack = No subgoals
REPEAT CONJ_TAC THEN REWRITE_TAC[thl]
REPEAT CONJ_TAC THEN TRY(REWRITE_TAC[thl] THEN NO_TAC)