AUGMENT_SIMPSET : thm -> simpset -> simpset
Augment context of a simpset with a list of theorems.
In their maximal generality, simplification operations in HOL Light (as invoked
by SIMP_TAC) are controlled by a `simpset'. Given a list of theorems thl
and a simpset ss, the call AUGMENT_SIMPSET thl ss augments the state of the
simpset, adding the theorems as new rewrite rules and also making any
provers in the simpset process the new context appropriately.
- FAILURE CONDITIONS
Never fails unless some of the simpset functions are ill-formed.
Mostly for experts wishing to customize the simplifier.
- SEE ALSO