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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
