*** 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