[opentheory-users] Standalone Tactics using OpenTheory

[Felix Breuer]

Hello Ramana, hello Joe,

I have read your article "Standalone Tactics using OpenTheory" with great
interest and I have two questions:

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.

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?

Thanks,
Felix

-- 
http://www.felixbreuer.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20121118/1f865ff4/attachment.html>