Re: [isabelle] Isabelle2014-RC2 available for testing
Am 06.08.14 13:11, schrieb Makarius:
Yes I figured that out, but my first go was just sledgehammer again
which worked fine. Later I did a find/replace which edited two more
On Wed, 6 Aug 2014, bnord wrote:
When opening my Development in Isabelle/jEdit 2014-RC2 I got some
(3-4) error markers that the theorem nat_add_commute was not found in
some metis commands. I cleared them manually until all error markers
were gone. Then when I restarted Isabelle/jEdit I got more error
markers of the same kind, cleared them again manually until all were
gone. But I still found 2 places were nat_add_commute was used using
search afterwards which were not marked as errors.
According to NEWS there was a renaming of nat_add_commute ~>
add.commute (and more like that).
No I wasn't sure just made the above observations. But I figured this
one out now, just noticed that for long documents the bar on the right
(whatever you call it) doesn't display markers for the whole document
but only for some part. You have to scroll through the whole document
after processing it to see whether there are any markers. This isn't
what one is used to from other editors with such a feature.
Are you sure that the proof commands that still referred to this
non-existing fact were actually applied successfully? I changed the
error recovery recently, actually going back to some suggestions of
yourself, but this change may now lead to some confusion.
This archive was generated by a fusion of
Pipermail (Mailman edition) and