*** 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
