Re: [isabelle] Confusing behavior of a paired set comprehension



No, a feature. Patterns may not contain repeated variables.

+1 vote for "bug".

The fact that Patterns may not contain repeated variables is perfectly fine. The fact that the first occurrence of a repeated variable is silently replaced by another variables is not fine.

But that's just the option of an Isabelle Newbie who got his proof wrong due to a surprising feature ;)

Best,
Jonas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.