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

The tactics with ASM in their name add the assumption list to the list of theorems used for dependent rewriting.

SEEALSO
HOL  Kananaskis-13