simpLib.SIMP_PROVE : simpset -> thm list -> term -> thm
STRUCTURE
simpLib
SYNOPSIS
Like SIMP_CONV, but converts boolean terms to theorem with same conclusion.
LIBRARY
simpLib
DESCRIPTION
SIMP_PROVE ss thml is equivalent to EQT_ELIM o SIMP_CONV ss thml.
FAILURE
Fails if the term can not be shown to be equivalent to true. May diverge.
EXAMPLE
Applying the tactic 
   ASSUME_TAC (SIMP_PROVE arith_ss [] ``x < y ==> x < y + 6``)
to the goal ?- x + y = 10 yields the new goal 
   x < y ==> x < y + 6 ?- x + y = 10
Using SIMP_PROVE here allows ASSUME_TAC to add a new fact, where the equality with truth that SIMP_CONV would produce would be less useful.

USES
SIMP_PROVE is useful when constructing theorems to be passed to other tools, where those other tools would prefer not to have theorems of the form |- P = T.
SEEALSO
SIMP_CONV, SIMP_RULE, SIMP_TAC
HOL  Kananaskis-14