1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\DOC EVERY_ASSUM
\TYPE {EVERY_ASSUM : thm_tactic -> tactic}
\SYNOPSIS
Sequentially applies all tactics given by mapping a function over the
assumptions of a goal.
\KEYWORDS
theorem-tactical, assumption.
\DESCRIBE
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)
}
\noindent If the goal has no assumptions, then {EVERY_ASSUM} has no effect.
\FAILURE
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.
\SEEALSO
ASSUM_LIST, MAP_EVERY, MAP_FIRST, THEN.
\ENDDOC
|
