REORDER_ANTS_MOD : (term list -> term list) -> (thm -> thm) -> thm -> thm
STRUCTURE
Drule
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
MODIFY_CONS g
FAILURE
Fails if
g
fails when applied to the consequent
SEEALSO
REORDER_ANTS
,
MODIFY_CONS
,
SPEC_ALL
,
GEN_ALL
,
UNDISCH
,
DISCH
HOL
Kananaskis-13