REORDER_ANTS_MOD

Drule.REORDER_ANTS_MOD : (term list -> term list) -> (thm -> thm) -> thm -> thm

Strips universal quantifiers and antecedents of implications, modifies the conclusion, and reorders the antecedents

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

See also

Drule.DISCH, Drule.GEN_ALL, Drule.REORDER_ANTS, Drule.SPEC_ALL, Drule.underAIs, Thm.UNDISCH