REWRITE_TAC : thm list -> tactic
# g `4 < 5`;; val it : goalstack = 1 subgoal (1 total) `4 < 5` # e(REWRITE_TAC[GT]);; val it : goalstack = 1 subgoal (1 total) `4 < 5`
# g `SUC n > 0`;; Warning: Free variables in goal: n val it : goalstack = 1 subgoal (1 total) `SUC n > 0` # e(REWRITE_TAC[GT; LT_0]);; val it : goalstack = No subgoals