REORDER_ANTS

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

Strips universal quantifiers and antecedents of implications and reorders the antecedents

   |- !x. a1 ==> !y. a2 ==> !z. a3 ==> !u. t
   ----------------------------------------- REORDER_ANTS rev
       |- a3 ==> a2 ==> a1 ==> t

Failure

No failure. Can leave the supplied theorem unchanged.

But a choice of f other than reordering a list of terms will give a result with assumptions remaining or superfluous antecedents

Comments

For simplicity, doesn’t try to reinsert quantifiers in appropriate places. If required, apply GEN_ALL to the resulting theorem.

See also

Drule.REORDER_ANTS_MOD, Drule.SPEC_ALL, Drule.GEN_ALL, Thm.UNDISCH, Drule.DISCH