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
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.