[isabelle-dev] Isabelle2011-test3 bugs
makarius at sketis.net
Thu Feb 3 15:25:04 CET 2011
On Thu, 3 Feb 2011, Sree Harsha Totakura wrote:
> I'm using the new Isabelle test candidate at
> http://www4.in.tum.de/~wenzelm/test/isa2011-test3/download.html on
> Ubuntu 10.04 with emacs23 and ran across an error.
> While proving a lemma in my theory in Proof General, it wouldn't let me
> advance over the lemma's proposition. It gets interrupted after
> sometime! It works fine in the older 2009 stable version of Isabelle.
> However, if I point the cursor at some arbitrary line in the lemma's
> proof and press the "Process to the cursor position" it works.
This sounds like one of the problems with Proof General that I've
addressed in the last minute, updating isa2011-test3/download.html
in-place without creating a new version name. So you might have an older
test version where this is still there.
Anyway, in the meantime we have official Isabelle2011 on
http://isabelle.in.tum.de and there is a good change that it works better.
More information about the isabelle-dev