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