[isabelle-dev] [isabelle] Confusing behavior of a paired set comprehension

Tobias Nipkow nipkow at in.tum.de
Wed Apr 4 12:07:37 CEST 2012

Am 04/04/2012 11:48, schrieb Tjark Weber:
> Adhering to the principle of least astonishment, I suspect an error
> message (or at least a warning) would be more helpful.

Isabelle's well-tried principle of least astonishment is not to give too many
helpful error messages or warnings ;-)

Actually, in this case it is not so easy to produce an error message because the
patterns are translated away with translations and the resulting lambda's are
perfectly legal.


More information about the isabelle-dev mailing list