&&
op bossLib.&& : simpset * thm list -> simpset
Also exported as BasicProvers.&&.
Infix operator for adding theorems into a simpset.
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
> val ss = boolSimps.bool_ss && pairLib.pair_rws;
val ss =
Included fragments (with 1 anonymous fragment [remove using name ""]):
BOOL, CONG, NOT, PURE, UNWIND
Rewrites (with 9 anonymous rewrites)
Other net names/keys:
.rewrite:COND_BOOL_CLAUSES.1, .rewrite:COND_BOOL_CLAUSES.2,
.rewrite:COND_BOOL_CLAUSES.3, .rewrite:COND_BOOL_CLAUSES.4,
.rewrite:EXCLUDED_MIDDLE'.1, .rewrite:EXISTS_REFL'.1,
.rewrite:EXISTS_UNIQUE_REFL'.1, .rewrite:NOT_AND'.1,
.rewrite:lift_disj_eq.1, .rewrite:lift_disj_eq.2,
[...Output elided...]
Comments
Of limited applicability since most of the tactics for rewriting already
include this functionality. However, applications of ZAP_TAC can
benefit.