[opentheory-users] deductAntisym and eqMp
rda at lemma-one.com
Thu Dec 5 14:18:16 UTC 2013
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.
More information about the opentheory-users