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 basic_net
\TYPE {basic_net : unit -> gconv net}
\SYNOPSIS
Returns the term net used to optimize access to default rewrites and
conversions.
\DESCRIBE
The HOL Light rewriter ({REWRITE_TAC} etc.) and simplifier ({SIMP_TAC} etc.)
have default sets of (conditional) equations and other conversions that are
applied by default, except in the {PURE_} variants. Internally, these are
maintained in a term net (see {enter} and {lookup} for more information), and a
call to {basic_net()} returns that net.
\FAILURE
Never fails.
\USES
Only useful for those who are delving deep into the implementation of
rewriting.
\SEEALSO
basic_convs, basic_rewrites, enter, lookup.
\ENDDOC
|
