Maps an inference rule over the assumptions of a goal.
DESCRIPTION
When applied to an inference rule f and a goal ({A1;...;An} ?- t),
the RULE_ASSUM_TAC tactical applies the inference rule to each of the
assumptions to give a new goal.
{A1,...,An} ?- t
==================================== RULE_ASSUM_TAC f
{f(.. |- A1),...,f(.. |- An)} ?- t
FAILURE CONDITIONS
The application of RULE_ASSUM_TAC f to a goal fails iff f fails when
applied to any of the assumptions of the goal.
COMMENTS
It does not matter if the goal has no assumptions, but in this case
RULE_ASSUM_TAC has no effect.