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
33
|
\DOC PURE_ASM_REWRITE_TAC
\TYPE {PURE_ASM_REWRITE_TAC : (thm list -> tactic)}
\SYNOPSIS
Rewrites a goal including the goal's assumptions as rewrites.
\KEYWORDS
tactic.
\DESCRIBE
{PURE_ASM_REWRITE_TAC} generates a set of rewrites from the supplied
theorems and the assumptions of the goal, and applies these in a
top-down recursive manner until no match is found. See
{GEN_REWRITE_TAC} for more information on the group of rewriting
tactics.
\FAILURE
{PURE_ASM_REWRITE_TAC} does not fail, but it can diverge in certain
situations. For limited depth rewriting, see
{PURE_ONCE_ASM_REWRITE_TAC}. It can also result in an invalid tactic.
\USES
To advance or solve a goal when the current assumptions are expected
to be useful in reducing the goal.
\SEEALSO
ASM_REWRITE_TAC, GEN_REWRITE_TAC, FILTER_ASM_REWRITE_TAC,
FILTER_ONCE_ASM_REWRITE_TAC, ONCE_ASM_REWRITE_TAC, ONCE_REWRITE_TAC,
PURE_ONCE_ASM_REWRITE_TAC, PURE_ONCE_REWRITE_TAC, PURE_REWRITE_TAC,
REWRITE_TAC, SUBST_TAC.
\ENDDOC
|
