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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and