SRW_TAC : ssfrag list -> thm list -> tactic
STRUCTURE
SYNOPSIS
A version of RW_TAC with an implicit simpset.
LIBRARY
bossLib
DESCRIPTION
A call to SRW_TAC [d1,...,dn] thlist produces the same result as
   RW_TAC (srw_ss() ++ d1 ++ ... ++ dn) thlist
FAILURE
When applied to a goal, the tactic resulting from an application of SRW_TAC may diverge.
COMMENTS
There are two reasons why one might prefer SRW_TAC to RW_TAC. Firstly, when a large number of datatypes are present in the TypeBase, the implementation of RW_TAC has to merge the attendant simplifications for each type onto its simpset argument each time it is called. This can be rather time-consuming. Secondly, the simpset returned by srw_ss() can be augmented with fragments from other sources than the TypeBase, using the functions augment_srw_ss and export_rewrites. This can make for a tool that is simple to use, and powerful because of all its accumulated simpset fragments.

Naturally, the latter advantage can also be a disadvantage: if SRW_TAC does too much because there is too much in the simpset underneath srw_ss(), then there is no way to get around this using SRW_TAC.

Typical invocations of SRW_TAC will be of the form

   SRW_TAC [][th1, th2,.. ]
The first argument, for lists of simpset fragments is for the inclusion of fragments that are not always appropriate. An example of such a fragment is numSimps.ARITH_ss, which embodies an arithmetic decision procedure for the natural numbers.
SEEALSO
HOL  Kananaskis-14