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
|
\DOC REWRITES_CONV
\TYPE {REWRITES_CONV : ('a * (term -> 'b)) net -> term -> 'b}
\SYNOPSIS
Apply a prioritized conversion net to the term at the top level.
\DESCRIBE
The underlying machinery in rewriting and simplification assembles
(conditional) rewrite rules and other conversions into a net, including a
priority number so that, for example, pure rewrites get applied before
conditional rewrites. If {net} is such a net (for example, constructed using
{mk_rewrites} and {net_of_thm}), then {REWRITES_CONV net} is a conversion that
uses all those conversions at the toplevel to attempt to rewrite the term. If a
conditional rewrite is applied, the resulting theorem will have an assumption.
This is the primitive operation that performs HOL Light rewrite steps.
\FAILURE
Fails when applied to the term if none of the conversions in the net are
applicable.
\SEEALSO
GENERAL_REWRITE_CONV, GEN_REWRITE_CONV, mk_rewrites, net_of_conv, net_of_thm,
REWRITE_CONV.
\ENDDOC
|
