op && : simpset * thm list -> simpset
STRUCTURE
SYNOPSIS
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.
SEEALSO
HOL  Trindemossen-1