<div dir="ltr"><div><div>I believe they are intended to be interpreted modulo alpha-convertibility, indeed.<br></div>(There's also a note at the top of the article specification saying Thm objects are interchangeable if terms in them are alpha-convertible.)<br>

</div>HOL4 also uses sets-up-to-alpha for the assumptions on a sequent.<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Dec 5, 2013 at 2:18 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>


<br>
Regards,<br>
<br>
Rob.<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>