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 the assumptions? If I (GEN_ALL o DISCH_ALL) I would get back to exactly where I started! :-)
Thanks, Haitao
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
