[isabelle-dev] Fwd: A possible bug with Isabelle 2013
makarius at sketis.net
Wed Feb 27 13:23:29 CET 2013
On Tue, 26 Feb 2013, Lawrence Paulson wrote:
> A student has forwarded this problem to me. It seems weird and unbelievable. What have I overlooked?
> I tidied it up slightly (see below) but I get the same error message.
> lemma "True"
> proof -
> have "True = (∃x. (λy. True) x)" by simp
> also have "... = (∃x. (λy. True) x)"
This is off-topic for isabelle-dev, it is about an official Isabelle
release, and has nothing to do with the Isabelle development process
itself. Our main "issue tracker" is isabelle-users.
When you say "bug" in the title, there is a already 50% chance that it is
just a misunderstanding by the user, and it is indeed the situation once
There might be technical reasons for misunderstandings, and ways to avoid
them without moving backwards and forgetting important lessons from the
past. But that case here is actually an FAQ, one for isabelle-users and
More information about the isabelle-dev