The Tutorial mentions the structure defCNF, in particular the function
defCNF.DEF_CNF_CONV in chapter 7 (page 123), but I don't think this
structure is built by default when one builds HOL.
This can cause some confusion.
I think it is available, though, in examples/HolCheck. Perhaps the Tutorial
should mention that, and how to build it.
On that note, I can't build examples/HolCheck because of this error:
> Error- in '/local/scratch/rk436/HOL/examples/muddy/MuddyCore.sml', line 6.
Structure (Dynlib) has not been declared Found near open Dynlib
Do I need to have Muddy or some other extra thing installed? If so, the
Tutorial should mention that as well (does it? - maybe I haven't read
closely enough..)
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
