Re: [isabelle] lexical matters
On Mon, 17 Jan 2011, mark at proof-technologies.com wrote:
I've known this "issue" ever since I got exposed to Isabelle for the
very first time, in summer 1993.
It puzzles me how little has been done about these things until now.
Are not people concerned that what is being displayed could be
There are other, more pressing problems. Sitting at a bare-bones ML
toplevel merely gives you an illusion of "direct" access to a system, but
there are still many things that can go wrong.
An LCF-style prover is reasonably correct by construction, independently
of concrete syntax input and output. Errors in the
internalization/externalization do not multiply as quickly as genuine
This archive was generated by a fusion of
Pipermail (Mailman edition) and