# HG changeset patch
# User wenzelm
# Date 1474204602 -7200
# Node ID cc15bd7c5396b31b170a9e670f37e183a0ad5a0e
# Parent  ca41b6670904e62b90f5d196069db8d7cbfe74c6
clarified notation;

diff -r ca41b6670904 -r cc15bd7c5396 NEWS
--- a/NEWS	Sun Sep 18 11:31:19 2016 +0200
+++ b/NEWS	Sun Sep 18 15:16:42 2016 +0200
@@ -231,6 +231,14 @@
 
 *** HOL ***
 
+* The unique existence quantifier no longer provides 'binder' syntax,
+but uses syntax translations (as for bounded unique existence). Thus
+iterated quantification \<exists>!x y. P x y with its slightly confusing
+sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
+pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
+(analogous existing notation \<exists>!(x, y)\<in>A. P x y). Potential
+INCOMPATIBILITY in rare situations.
+
 * Renamed session HOL-Multivariate_Analysis to HOL-Analysis.
 
 * Moved measure theory from HOL-Probability to HOL-Analysis. When importing
diff -r ca41b6670904 -r cc15bd7c5396 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Sep 18 11:31:19 2016 +0200
+++ b/src/HOL/HOL.thy	Sun Sep 18 15:16:42 2016 +0200
@@ -99,12 +99,24 @@
 definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
   where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
 
-definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>!" 10)
+definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
 
 
 subsubsection \<open>Additional concrete syntax\<close>
 
+syntax (ASCII)
+  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
+syntax (input)
+  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
+syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
+translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
+
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs_tr' @{const_syntax Ex1} @{syntax_const "_Ex1"}]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
+
 abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>" 10)
   where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)"
 
@@ -158,13 +170,11 @@
 
 notation (ASCII)
   All  (binder "ALL " 10) and
-  Ex  (binder "EX " 10) and
-  Ex1  (binder "EX! " 10)
+  Ex  (binder "EX " 10)
 
 notation (input)
   All  (binder "! " 10) and
-  Ex  (binder "? " 10) and
-  Ex1  (binder "?! " 10)
+  Ex  (binder "? " 10)
 
 
 subsubsection \<open>Axioms and basic definitions\<close>