ONCE_SIMP_RULE : thm list -> thm -> thm

SYNOPSIS
Simplify conclusion of a theorem once by conditional contextual rewriting.

DESCRIPTION
A call ONCE_SIMP_RULE thl (|- tm) will return |- tm' where tm' results from applying the theorems in thl as (conditional) rewrite rules, as well as built-in simplifications (see basic_rewrites and basic_convs). For more details on this kind of conditional rewriting, see SIMP_CONV. The ONCE prefix indicates that the first applicable terms in a toplevel term will be simplified once only, though conditional subgoals generated will be simplified repeatedly.

FAILURE CONDITIONS
Never fails, but may return the initial theorem unchanged.

SEE ALSO
ASM_SIMP_TAC, SIMP_CONV, SIMP_RULE, SIMP_TAC.