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 quickly.

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 MHonArc.