Re: [isabelle] lexical matters
On Mon, 17 Jan 2011, mark at proof-technologies.com wrote:
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.
You can implement your own in user space. These things are not part of
the kernel. Even the ML toplevel pretty printer can be modified in user
Anyway, do you now the funny paper about by Freek Wiedijk, UITP 2010?
I've known this "issue" ever since I got exposed to Isabelle for the very
first time, in summer 1993.
This archive was generated by a fusion of
Pipermail (Mailman edition) and