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
|
\DOC PURE_SIMP_TAC
\TYPE {PURE_SIMP_TAC : thm list -> tactic}
\SYNOPSIS
Simplify a goal repeatedly by conditional contextual rewriting without default
simplifications.
\DESCRIBE
When applied to a goal {A ?- g}, the tactic {PURE_SIMP_TAC thl} returns a new
goal {A ?- g'} where {g'} results from applying the theorems in {thl} as
(conditional) rewrite rules. The {PURE} prefix means that it does not apply the
built-in simplifications (see {basic_rewrites} and {basic_convs}). For more
details, see {SIMP_CONV}.
\FAILURE
Never fails, though may not change the goal if no simplifications are
applicable.
\COMMENTS
To add the assumptions of the goal to the rewrites, use {PURE_ASM_SIMP_TAC} (or
just {ASM PURE_SIMP_TAC}).
\SEEALSO
ASM, ASM_SIMP_TAC, mk_rewrites, ONCE_SIMP_CONV, REWRITE_TAC, SIMP_CONV,
SIMP_RULE.
\ENDDOC
|
