Hi，
I have been generated a proof article file from a HOL Light theory file. But I
found that the opentheory can’t use the large .ml file to generate the proof
articles,for example vector.ml.When I run the command “opentheory compile”,the
screen appeard the erroe of “out of memory”.Can you tell me why and how to
solve it please?
And now I can’t read the proof article file into my theorem prover(HOL4).Before
I read your paper entitled “OpenTheory: Package Management for Higher Order
Logic Theories”, it was reference to “These HOL Light theories were read into
HOL4 by a tool for reading articles implemented by Quinn Yee Qin The.”Can you
tell me the method about “How can I use the tool of reader read the proof
article file?”
I'm looking forward for your reply. Thank you very much!
Best wishes,
Amy
------------------------------------------------------------------------------
Download Intel® Parallel Studio Eval
Try the new software tools for yourself. Speed compiling, find bugs
proactively, and fine-tune applications for parallel performance.
See why Intel Parallel Studio got high marks during beta.
http://p.sf.net/sfu/intel-sw-dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
