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

Tjark Weber webertj at in.tum.de
Wed Apr 4 11:48:27 CEST 2012

On Wed, 2012-04-04 at 11:19 +0200, Tobias Nipkow wrote:
> No, a feature. Patterns may not contain repeated variables.

But this is not being enforced; instead, repeated variables are silently

Adhering to the principle of least astonishment, I suspect an error
message (or at least a warning) would be more helpful.

Best regards,

More information about the isabelle-dev mailing list