ASM_SIMP_RULE : simpset -> thm list -> thm -> thm
STRUCTURE
SYNOPSIS
Simplifies a theorem, using the theorem’s assumptions as rewrites in addition to the provided rewrite theorems and simpset.
LIBRARY
simpLib
FAILURE
Never fails, but may diverge.
EXAMPLE
- ASM_SIMP_RULE bool_ss [] (ASSUME (Term `x = 3`))
> val it =  [.] |- T : thm

USES
The assumptions can be used to simplify the conclusion of the theorem. For example, if the conclusion of a theorem is an implication, the antecedent together with the hypotheses may help simplify the conclusion.
SEEALSO
HOL  Kananaskis-13