Sequentially applies all tactics given by mapping a function over the
assumptions of a goal.
DESCRIPTION
When applied to a theorem-tactic f and a goal ({A1;...;An} ?- C), the
EVERY_ASSUM tactical maps f over the list of assumptions then
applies the resulting tactics, in sequence, to the goal:
EVERY_ASSUM f ({A1;...;An} ?- C)
= (f(.. |- A1) THEN ... THEN f(.. |- An)) ({A1;...;An} ?- C)
If the goal has no assumptions, then EVERY_ASSUM has no effect.
FAILURE CONDITIONS
The application of EVERY_ASSUM to a theorem-tactic and a goal fails
if the theorem-tactic fails when applied to any of the assumptions of the goal,
or if any of the resulting tactics fail when applied sequentially.