Eliminates a conjunctive antecedent in favour of implication.
DESCRIPTION
When applied to a term of the form (t1 /\ t2) ==> t, the conversion
ANTE_CONJ_CONV returns the theorem:
|- (t1 /\ t2 ==> t) = (t1 ==> t2 ==> t)
FAILURE
Fails if applied to a term not of the form "(t1 /\ t2) ==> t".
USES
Somewhat ad-hoc, but can be used (with CONV_TAC) to transform a goal of the
form ?- (P /\ Q) ==> R into the subgoal ?- P ==> (Q ==> R), so that only
the antecedent P is moved into the assumptions by DISCH_TAC.