DEP_PURE_REWRITE_TAC : thm list -> tactic
STRUCTURE
SYNOPSIS
Rewrites a goal using implications of equalites, adding proof obligations as required.
DESCRIPTION
DEP_PURE_REWRITE_TAC is to DEP_REWRITE_TAC what PURE_REWRITE_TAC is to REWRITE_TAC.

The tactics including PURE in their name will only use the listed theorems for all rewriting; otherwise, the standard rewrites are used for normal rewriting, but they are not considered for dependent rewriting.

SEEALSO
HOL  Kananaskis-14