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 renamed. Adhering to the principle of least astonishment, I suspect an error message (or at least a warning) would be more helpful. Best regards, Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
