set_basic_congs : thm list -> unit

- SYNOPSIS
- Change the set of basic congruences used by the simplifier.
- DESCRIPTION
- 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 CONDITIONS
- Never fails.
- COMMENTS
- Normally, users only need to extend the congruences; for an example of how to do that see extend_basic_congs.
- SEE ALSO
- basic_congs, extend_basic_congs, SIMP_CONV, SIMP_RULE, SIMP_TAC.