Hello Ramana, hello Joe,<div><br></div><div>I have read your article "Standalone Tactics using OpenTheory" with great interest and I have two questions:</div><div><br></div><div>1) Is the code for the system you describe (both client and the HOL4 and HOL Light "servers") available somewhere? I'd like to try this out myself.</div>
<div><br></div><div>2) I do not quite understand how the goals that are sent to the server are encoded using OpenTheory. As far as I understand an OT article provides facilities for encoding assumptions and theorems. How do goals fit into the picture?</div>
<div><br></div><div>Thanks,</div><div>Felix<br clear="all"><div><br></div>-- <br><a href="http://www.felixbreuer.net">http://www.felixbreuer.net</a><br>
</div>