PURE_REWRITE_TAC : thm list -> tactic
# g `b <=> T`;; Warning: Free variables in goal: b val it : goalstack = 1 subgoal (1 total) `b <=> T` # e(PURE_REWRITE_TAC[]);; val it : goalstack = 1 subgoal (1 total) `b <=> T` # e(REWRITE_TAC[]);; val it : goalstack = 1 subgoal (1 total) `b`