[isabelle-dev] NEWS: syntax for unique existence quantifier

[Makarius]

*** HOL ***

* The unique existence quantifier no longer provides 'binder' syntax,
but uses syntax translations (as for bounded unique existence). Thus
iterated quantification ∃!x y. P x y with its slightly confusing
sequential meaning ∃!x. ∃!y. P x y is no longer possible. Instead,
pattern abstraction admits simultaneous unique existence ∃!(x, y). P x y
(analogous existing notation ∃!(x, y)∈A. P x y). Potential
INCOMPATIBILITY in rare situations.


This refers to Isabelle/cc15bd7c5396. In e4fdf9580372 there is an
example of using the unique existence of a pair, but such cases are very
rare.

Note that the tuple pattern support is a natural consequence of using
translations instead of 'binder'. It has been there for a long time for
the bounded quantifier, e.g.

lemma "∃!(x, y) ∈ {(a, b)}. True" by auto


	Makarius