Dear hol-info/hol-developers, Some readers may be interested in an application of Hol to verify the correctness of a parser generator for all context-free grammars:
http://www.cs.le.ac.uk/people/tr61/parsing/ (hol-developers only) I'd like to put the proof development in the Hol SVN as an example, but I don't want to "tidy" the proofs. Would people mind if I did this? Also, I have collected many lemmas that I would like to include in the relevant Hol script files, but again I don't want to "tidy" the proofs. Is there a way to do this cleanly? Thanks in advance Tom ------------------------------------------------------------------------------ WhatsUp Gold - Download Free Network Management Software The most intuitive, comprehensive, and cost-effective network management toolset available today. Delivers lowest initial acquisition cost and overall TCO of any competing solution. http://p.sf.net/sfu/whatsupgold-sd _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
