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
|
\DOC set_basic_congs
\TYPE {set_basic_congs : thm list -> unit}
\SYNOPSIS
Change the set of basic congruences used by the simplifier.
\DESCRIBE
The HOL Light simplifier (as invoked by {SIMP_TAC} etc.) uses congruence rules
to determine how it uses context when descending through a term. These are
essentially theorems showing how to decompose one equality to a series of other
inequalities in context. A call to {set_basic_congs thl} sets the congruence
rules to the list of theorems {thl}.
\FAILURE
Never fails.
\COMMENTS
Normally, users only need to extend the congruences; for an example of how to
do that see {extend_basic_congs}.
\SEEALSO
basic_congs, extend_basic_congs, SIMP_CONV, SIMP_RULE, SIMP_TAC.
\ENDDOC
|
