Instead of writing the simpler SIMP_CONV std_ss thmlist, one could
write
SIMP_CONV (std_ss ++ rewrites thmlist) []
More plausibly, rewrites can be used to create commonly
used ssfrag values containing a great number of rewrites. This is
how the basic system’s various ssfrag values are constructed where
those values consist only of rewrite theorems.