Re: [isabelle] lexical matters



>> Is there a printing mode for type-annotating constants and/or variables
>> with their types (like in HOL4)?  I'm concerned about the risk of
>> statements being displayed in a misleading way.
>
> ...
> Anyway, do you now the funny paper about "Pollack-inconsistency" by Freek
Wiedijk, UITP 2010?

Yes thanks.  In fact my HOL system, HOL Zero
(http://proof-technologies.com/holzero.html), deals with all these issues
(or so I claim - there is a $100 bounty for anyone that spots a problem).  I
was wondering how well Isabelle fared.

> 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?

Mark.





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