Re: [isabelle] New error messages in Isabelle 2013
On 2/1/2013 6:18 AM, Makarius wrote:
This means you can explore that recursively by hovering over formal
input and output -- this is now mostly uniform in Isabelle2013. This
unfolds a massive tree of information, or rather a large forest, by
walking a few steps into some of its paths.
Thanks for the explanation. And we all know how much we love hyperlinks.
This is definitely a "friendly IDE" feature you've added. It's good when
information comes to me via hyperlinks, rather than me having to go to
In case others might not have noticed yet, the hyperlinks are grey boxes
with a line around them, rather than just grey boxes.
But the way it works is that some people don't forgo the old for the
new, they keep the old and use the new also. But it may be the economics
of IDEs, that the old has to be sacrificed for the new. And that's why
there's a thriving software utility market. Microsoft gets rid of the
taskbar and start button in Windows 8, and someone produces a utility to
put it all back.
Of course, there are endless possibilities to refine this further. An
obvious question is: What is a succinct "digest" (as output text) to
give you a types / sorts environment for some formal output. Old
show_types / show_sorts are traditionally very crude here. This is
only a starting point for further reworking of these ancient
mechanisms. In particular, I hope to see certain improvements done
for current sledgehammer isar_proofs output to be taken into account
Sounds like a lot of work.
This archive was generated by a fusion of
Pipermail (Mailman edition) and