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

[Lawrence Paulson]

It's absolutely appropriate to send a message to 20 experts rather than 600 users when the latter are very unlikely to have a clue what's going on here.

Anyway, it is a development matter. A behaviour where "..." denotes something other than the previous right-hand side needs to be fixed.

Larry

On 27 Feb 2013, at 12:23, Makarius <makarius at sketis.net> wrote:

> 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