[isabelle-dev] Isabelle2011-test3 bugs

[Sree Harsha Totakura]

Hi,

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.

I also observe that sledgehammer sometimes couldn't find proofs where it is
able to in the Isabelle-2009 stable version.

Regards,
Sree Harsha Totakura
MS Informatics
Technische Universität München
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110203/f1e5e262/attachment.html>