----------------------------------------------------------------------
SRW_TAC                                                      (bossLib)
----------------------------------------------------------------------
SRW_TAC : ssfrag list -> thm list -> tactic

SYNOPSIS
A version of {RW_TAC} with an implicit {simpset}.

KEYWORDS
simplification

LIBRARY
bossLib

DESCRIBE
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
bossLib.srw_ss, bossLib.augment_srw_ss, BasicProvers.export_rewrites,
simpLib.SSFRAG.

----------------------------------------------------------------------