ASM_REWRITE_TAC : thm list -> tactic
# g `P ==> (P /\ Q /\ R <=> R /\ Q /\ P)`;; Warning: Free variables in goal: P, Q, R val it : goalstack = 1 subgoal (1 total) `P ==> (P /\ Q /\ R <=> R /\ Q /\ P)` # e DISCH_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`P`] `P /\ Q /\ R <=> R /\ Q /\ P` # e(ASM_REWRITE_TAC[]);; val it : goalstack = 1 subgoal (1 total) 0 [`P`] `Q /\ R <=> R /\ Q`