Rewrites a theorem once with only the given list of rewrites.
DESCRIPTION
PURE_ONCE_REWRITE_RULE generates rewrites from the list of theorems
supplied by the user, without including the tautologies given in
implicit_rewrites. The applicable rewrites are employeded once, without
entailing in a recursive search for matches over the theorem.
See GEN_REWRITE_RULE for more details about rewriting strategies in
HOL.