ASM_SIMP_TAC : simpset -> thm list -> tactic
STRUCTURE
bossLib
SYNOPSIS
Simplifies a goal using the simpset, the provided theorems, and the goal’s assumptions.
LIBRARY
simpLib
DESCRIPTION
ASM_SIMP_TAC does a simplification of the goal, adding both the assumptions and the provided theorem to the given simpset as rewrites. This simpset is then applied to the goal in the manner explained in the entry for SIMP_CONV.

ASM_SIMP_TAC is to SIMP_TAC, as ASM_REWRITE_TAC is to REWRITE_TAC.

FAILURE
ASM_SIMP_TAC never fails, though it may diverge.
EXAMPLE
The simple goal x < y ?- x + y < y + y can be proved by using bossLib.arith_ss and the assumption by 
   ASM_SIMP_TAC bossLib.arith_ss []
SEEALSO
++, bool_ss, FULL_SIMP_TAC, mk_simpset, SIMP_CONV, SIMP_TAC, ASM_REWRITE_TAC, VAR_EQ_TAC
HOL  Kananaskis-13