Re: [isabelle] lexical matters

On Mon, 17 Jan 2011, mark at 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 misleading?

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 logical errors.


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