Infix operator for adding theorems into a simpset.
DESCRIPTION
It is occasionally necessary to extend an existing simpset ss with a
collection rwlist of new rewrite rules. To achieve this, one
applies the && function via ss && rwlist.
FAILURE
Never fails.
EXAMPLE
- open bossLib;
... <output elided> ...
- val ss = boolSimps.bool_ss && pairTheory.pair_rws;
> val ss = <simpset> : simpset
COMMENTS
Of limited applicability since most of the tactics for rewriting
already include this functionality. However, applications of ZAP_TAC
can benefit.