&&

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.

See also

simpLib.++, simpLib.SIMP_CONV, bossLib.RW_TAC