<div dir="ltr">OpenTheory theorem hypotheses are indeed supposed to be represented by a set of terms modulo alpha-equivalence: I've added a note to that effect in the description of the thm type in<div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html">http://www.gilith.com/research/opentheory/article.html</a><br>
</div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Dec 5, 2013 at 2:33 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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="HOEnZb"><div class="h5"><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" target="_blank">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>
</div></div><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>
<br></blockquote></div><br></div>