Re: [isabelle] lexical matters

On Mon, 2011-01-17 at 22:34 +0000, mark at wrote:
> 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?

Well, I for one think it's an unsatisfying design flaw in (some)
existing provers that one cannot trust their output.

In practice, however, this becomes a potential problem only when you
want to check a proof from an untrustworthy source.  (Proof objects
provide a partial solution here.)

As long as you assume a non-malicious user who wants to create a valid
machine-checked proof, it is not much of an issue.

Kind regards,

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