ONCE_ASM_REWRITE_TAC : thm list -> tactic
# g `a = b /\ b = c ==> (P a b <=> P c a)`;; Warning: inventing type variables Warning: Free variables in goal: P, a, b, c val it : goalstack = 1 subgoal (1 total) `a = b /\ b = c ==> (P a b <=> P c a)` # e STRIP_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`a = b`] 1 [`b = c`] `P a b <=> P c a`
# e(ONCE_ASM_REWRITE_TAC[]);; val it : goalstack = 1 subgoal (1 total) 0 [`a = b`] 1 [`b = c`] `P b c <=> P c b`