Simplify conclusion of goal once by conditional contextual rewriting.
DESCRIPTION
When applied to a goal A ?- g, the tactic ONCE_SIMP_TAC thl returns a new
goal A ?- g' where g' 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.
Moreover, in contrast to the other simplification tactics, any unsolved
subgoals arising from conditions on rewrites will be split off as new goals,
allowing simplification to proceed more interactively.
FAILURE CONDITIONS
Never fails, though may not change the goal if no simplifications are
applicable.