Re: [isabelle] A few questions about Isabelle2013
On Tue, 15 Jan 2013, Alfio Martini wrote:
So far I am quite happy with this new version of Isabelle.
BTW, it is not a vew version of Isabelle yet, just a packaging test I made
in preparation of the coming release. It was leaked from isabelle-dev to
So it is pretty close to what should become Isabelle2013 during the next 4
weeks, or so. I hope to be able to start official Isabelle2013-RC1
testing at the end of this week. Right now we should count the above as
totally unofficial RC0. As you continue testing any of these versions, it
is important to update to consecutive release candidates whenever they
appear, to avoid getting stuck with these not fully finished snapshots.
Last time in the preparation of Isabelle2012, I introduced some small
problems in later release candidates as reaction to observation to earlier
ones. We need to avoided such accidents this time.
* Configuration option show_markup controls direct inlining of markup
into the printed representation of formal entities --- notably type
and sort constraints. This enables Prover IDE users to retrieve that
information via tooltips in the output window, for example.
It seems that, at least for constant functions, one is not able to see
the type of the constant in the tooltip window (only the theory where it
is defined) as opposed to the the corresponding one in the normal edit
window (after Ctrl+hover)..
I attach two images, where the situation described above can be clearly
Is this still a restriction or maybe a lack of proper configuration from
The parse vs. print phases of logical terms are not fully symmetric. It
is just an accident that parse manages to report on result types produced
by type-inference, but print omits that information.
So it is just one of these things that still don't work for the coming
This archive was generated by a fusion of
Pipermail (Mailman edition) and