[isabelle-dev] [isabelle] Confusing behavior of a paired set comprehension
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.
More information about the isabelle-dev