ses implicational theorems like this first, and then
> basically applies MATCH_MP_TAC.
>
>
>
> Michael
>
>
>
> *From: *Haitao Zhang
> *Date: *Friday, 1 March 2019 at 11:03
> *To: *hol-info
> *Subject: *[Hol-info] MATCH_MP_TAC and canonical implication form
>
>
I have a theorem that is in a form like !x y z. a ==> b ==> c ==> d and I
would like to match d to the goal. It seems that I need to convert all the
antecedents into a conjunction first. I can (UNDISCH_ALL o SPEC_ALL) to
move everything to the assumptions. But how do I get the conjunctions of
all t
