Hi Tom,
That would be fine. If you feel a need to mention untidy proofs,
just add a mention in the README file. For lemmas, they
can sometimes just be put in auxiliary files that the xScript.sml
file depends on. I'm not sure if that's what you are asking ...
Konrad.
On Tue, Apr 26, 2011 at 11:20 AM, Tom Ridge <
tom.j.ridge+hol-develop...@googlemail.com> wrote:
> 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-developers mailing list
> hol-develop...@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-developers
>
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
