REORDER_ANTS_MOD : (term list -> term list) -> (thm -> thm) -> thm -> thm
STRUCTURE
SYNOPSIS
Strips universal quantifiers and antecedents of implications, modifies the conclusion, and reorders the antecedents
DESCRIPTION
REORDER_ANTS_MOD f g combines the effects of REORDER_ANTS_MOD f and applies the function g to the ultimate consequent of the theorem, as does underAIs.
FAILURE
Fails if g fails when applied to the consequent
SEEALSO
HOL  Trindemossen-1