bossLib.SRULE

A call to SRULE ths th simplifies the theorem th using the standard simpset (accessible through a call to srw_ss()) and the theorems ths, returning the simplified theorem.

The implementation of SRULE is

   fun SRULE ths th = SIMP_RULE (srw_ss()) ths th

The fact that this definition is not eta-reduced means that partial applications of SRULE will continue to pick up the current value of srw_ss() when they are eventually fully applied, rather than bake in the value from the time of the partial application.