Re: [isabelle] lexical matters



On 19/01/11 14:04, mark at proof-technologies.com wrote:

I never thought that advocating a trustworthy pretty printer would be so
controversial!!!

It's just not an interesting problem.  We can solve it trivially by writing everything out in sexp-like notation.  ACL2 is demonstrably an acceptable format for security-critical validation, and this is all the pretty-printing they have.

Moreover, with proof terms (in Isabelle) and things like OpenTheory for the 3 HOLs, we can avoid having to look at clients' ML code.

Michael





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.