1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
\DOC ONCE_SIMP_RULE
\TYPE {ONCE_SIMP_RULE : thm list -> thm -> thm}
\SYNOPSIS
Simplify conclusion of a theorem once by conditional contextual rewriting.
\DESCRIBE
A call {ONCE_SIMP_RULE thl (|- tm)} will return {|- 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_CONV}. 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 the initial theorem unchanged.
\SEEALSO
ASM_SIMP_TAC, SIMP_CONV, SIMP_RULE, SIMP_TAC.
\ENDDOC
|
