[opentheory-users] deductAntisym and eqMp

[Rob Arthan]

The specifications of deductAntisym and eqMp use set operations on the assumptions. Are these intended to be interpreted modulo alpha-convertibility? (ProofPower and HOL Light both treat the assumptions as ordered sets  using  alpha-convertibility as the equality test when inserting and deleting elements, but I don't know about HOL4.) If the answer is no, then a reader for ProofPower or HOL Light is going to have to use some fairly horrid tricks.

Regards,

Rob.