RULE_ASSUM_TAC : (thm -> thm) -> tactic

SYNOPSIS

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.