[isabelle-dev] Fwd: A possible bug with Isabelle 2013

[Makarius]

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)"
> oops

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 
again.

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 
not isabelle-dev.


 	Makarius