1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
\DOC ONCE_SIMP_CONV
\TYPE {ONCE_SIMP_CONV : thm list -> conv}
\SYNOPSIS
Simplify a term once by conditional contextual rewriting.
\DESCRIBE
A call {ONCE_SIMP_CONV thl tm} will return {|- tm = tm'} where {tm'} results
from applying the theorems in {thl} as (conditional) rewrite rules, as well as
built-in simplifications (see {basic_rewrites} and {basic_convs}). For more
details on this kind of conditional rewriting, see {SIMP_TAC}. The {ONCE}
prefix indicates that the first applicable terms in a toplevel term will be
simplified once only, though conditional subgoals generated will be simplified
repeatedly.
\FAILURE
Never fails, but may return a reflexive theorem {|- tm = tm} if no
simplifications can be made.
\SEEALSO
ASM_SIMP_TAC, SIMP_RULE, SIMP_TAC.
\ENDDOC
|
