[isabelle-dev] Isabelle2011-test3 bugs

[Makarius]

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.


 	Makarius