ss_of_prover : (strategy -> strategy) -> simpset -> simpset

Change the method of prover application in a simpset.

In their maximal generality, simplification operations in HOL Light (as invoked by SIMP_TAC) are controlled by a `simpset', which may contain conditional and unconditional rewrite rules, conversions and provers for conditions, as well as a determination of how to use the prover on the conditions and how to process theorems into rewrites. The default `prover use' method is to first recursively apply all the simplification to conditions and then try the provers, if any, one by one until one succeeds. It is unusual to want to change this, but if desired you can do it with ss_of_prover str ss.

Never fails.

mk_rewrites, SIMP_CONV, ss_of_congs, ss_of_conv, ss_of_maker, ss_of_provers, ss_of_thms.