Hi all.
I’m currently having a problem about using the Holmake tool on Windows XP. I
tried to compile a script which all the theorems we had proved interactively,
and I added “open HolKernel boolLib Parse bossLib” ,new_theory and
export_theory to the script.When I running it, I can see the HOL message
“Created theory”, “Saved definition” and “Saved theorem”, but files didn’t
exported finally.
I want to know what’s the point to use Holmake on Windows.
Thank you very much, and have a good day.
Arthur.
------------------------------------------------------------------------------
All the data continuously generated in your IT infrastructure
contains a definitive record of customers, application performance,
security threats, fraudulent activity, and more. Splunk takes this
data and makes sense of it. IT sense. And common sense.
http://p.sf.net/sfu/splunk-novd2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
