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
31
32
|
\DOC RULE_ASSUM_TAC
\TYPE {RULE_ASSUM_TAC : (thm -> thm) -> tactic}
\SYNOPSIS
Maps an inference rule over the assumptions of a goal.
\KEYWORDS
tactic, assumption, rule.
\DESCRIBE
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
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.
\SEEALSO
ASSUM_LIST, MAP_EVERY, MAP_FIRST, POP_ASSUM_LIST.
\ENDDOC
|
