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
29
30
|
\DOC ss_of_conv
\TYPE {ss_of_conv : term -> conv -> simpset -> simpset}
\SYNOPSIS
Add a new conversion to a simpset.
\DESCRIBE
In their maximal generality, simplification operations in HOL Light (as invoked
by {SIMP_TAC}) are controlled by a `simpset', which may contain conditional and
unconditional rewrite rules, conversions and provers for conditions, as well as
a determination of how to use the prover on the conditions and how to process
theorems into rewrites. A call {ss_of_conv pat cnv ss} adds the conversion
{cnv} to the simpset {ss} to yield a new simpset, restricting the initial
filtering of potential subterms to those matching {pat}.
\FAILURE
Never fails.
\EXAMPLE
{
# ss_of_conv `x + y:num` NUM_ADD_CONV empty_ss;;
...
}
\SEEALSO
mk_rewrites, SIMP_CONV, ss_of_congs, ss_of_maker, ss_of_prover, ss_of_provers,
ss_of_thms.
\ENDDOC
|
