1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
\DOC SIMP_RULE
\TYPE {SIMP_RULE : thm list -> thm -> thm}
\SYNOPSIS
Simplify conclusion of a theorem repeatedly by conditional contextual
rewriting.
\DESCRIBE
A call {SIMP_CONV 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}.
\FAILURE
Never fails, but may return the input theorem unchanged if no simplifications
were applicable.
\SEEALSO
ONCE_SIMP_RULE, SIMP_CONV, SIMP_TAC.
\ENDDOC
|
