Jon, Your file does not show what you were trying to do with LEMMA_T, or what you actually did, so its hard to offer much help.
"lemma_tac" is easier to understand that "LEMMA_T", so you could try doing it with "lemma_tac" first. (you can always collapse it down to an application of LEMMA_T once you have succeeded in proving the lemma using "lemma_tac"). Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
