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 ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and