[opentheory-users] deductAntisym and eqMp

[Ramana Kumar]

I believe they are intended to be interpreted modulo alpha-convertibility,
indeed.
(There's also a note at the top of the article specification saying Thm
objects are interchangeable if terms in them are alpha-convertible.)
HOL4 also uses sets-up-to-alpha for the assumptions on a sequent.


On Thu, Dec 5, 2013 at 2:18 PM, Rob Arthan <rda at lemma-one.com> wrote:

> 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.
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131205/2416d66b/attachment.html>