Re: [isabelle] sorry in innocent blue?
On Tue, 13 May 2014, Tobias Nipkow wrote:
I just spent more than half an hour trying to figure out where the
problem with my (long) poof was after I had discovered that the
proposition was definitely not true. Eventually I found a single sorry
was left, attached to a wrong claim. If sorry - which is definietly
dangerous - had a dangerous colour, I would have spotted it more
In all official releases from 2013 there should be a "bad" markup for
sorry, after it was processed by the prover. That is neither an error nor
a warning (so it does not show up in the buffer overview column nor the
theories overview panel), but it has a thick red background and some
tooltip to tell the reason for the relative "badness".
If that special rendering was not to be seen, there might have been
something wrong elsewhere.
This archive was generated by a fusion of
Pipermail (Mailman edition) and