Re: [isabelle] Isabelle2015-RC0 available for testing



Dear Makarius

I found a "feature request" for the jEdit interface:
I loaded WordLemmaBucket from autocorres, a file with 5900 lines.
There are at least two errors  near the end of the file when loading
with 2015-RC0. However, it is nearly impossible to locate the errors
in the .thy. Is it possible to have some sort of "jump to next error"
or an automatic jump to the error when I click on the red spot (left
of the jEdit scroll bar)?
Also, when I have an error in my theory, e.g. writing "where f=..."
but in 2015-RC0 it should be "where f1=...", only the "f" is
underlined, this makes the error quite hard to spot for me.

Forther minor observations:
* Case_def no longer exists (and I guess not needed)
* when I type sledgehammer (not using the panel), it seems as it is
only tries cvc4 and remote_vampire, is it possible to add a bit more

Another question: Sometimes I have some helper lemmas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.