1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
\DOC ASM_SIMP_TAC
\TYPE {ASM_SIMP_TAC : thm list -> tactic}
\SYNOPSIS
Perform simplification of goal by conditional contextual rewriting using
assumptions and built-in simplifications.
\DESCRIBE
A call to {ASM_SIMP_TAC[theorems]} will apply conditional contextual rewriting
with {theorems} and the current assumptions of the goal to the goal's
conclusion, as well as the default simplifications (see {basic_rewrites} and
{basic_convs}). For more details on this kind of rewriting, see {SIMP_CONV}. If
the extra generality of contextual conditional rewriting is not needed,
{REWRITE_TAC} is usually more efficient.
\FAILURE
Never fails, but may loop indefinitely.
\SEEALSO
ASM_REWRITE_TAC, SIMP_CONV, SIMP_TAC, REWRITE_TAC.
\ENDDOC
|
