# HG changeset patch
# User wenzelm
# Date 1474214368 -7200
# Node ID 9f8325206465ac59e7205372ca2230958109a8f7
# Parent  d00d4f399f055b95f029a4f7f198e4e1f5262a96
clarified notation: iterated quantifier is negated as one chunk;

diff -r d00d4f399f05 -r 9f8325206465 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Sep 18 16:59:15 2016 +0200
+++ b/src/HOL/HOL.thy	Sun Sep 18 17:59:28 2016 +0200
@@ -117,11 +117,13 @@
 \<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)"
+syntax
+  "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
+  "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
+translations
+  "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
+  "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
 
-abbreviation Not_Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>!" 10)
-  where "\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)"
 
 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
   where "x \<noteq> y \<equiv> \<not> (x = y)"