Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
ASM : (thm list -> tactic) -> thm list -> tactic

SYNOPSIS
Augments a tactic's theorem list with the assumptions.

DESCRIPTION
If tac is a tactic that expects a list of theorems as its arguments, e.g. MESON_TAC, REWRITE_TAC or SET_TAC, then ASM tac converts it to a tactic where that list is augmented by the goal's assumptions.

FAILURE CONDITIONS
Never fails (though the resulting tactic may do).

EXAMPLE
The inbuilt ASM_REWRITE_TAC is in fact defined as just ASM REWRITE_TAC.

SEE ALSO
ASSUM_LIST, FREEZE_THEN, HYP, MESON_TAC, REWRITE_TAC, SET_TAC.