# HG changeset patch
# User wenzelm
# Date 1457207251 -3600
# Node ID d32c23d29968943c99734c0bab80bbf474ef096f
# Parent  6383440f41a819b9b4b5fc863185378fa05d854e
abbreviations for \<nexists>;

diff -r 6383440f41a8 -r d32c23d29968 NEWS
--- a/NEWS	Sat Mar 05 19:58:56 2016 +0100
+++ b/NEWS	Sat Mar 05 20:47:31 2016 +0100
@@ -23,6 +23,11 @@
 
 *** HOL ***
 
+* New abbreviations for negated existence (but not bounded existence):
+
+  \<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
+  \<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
+
 * The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
 has been removed for output. It is retained for input only, until it is
 eliminated altogether.
diff -r 6383440f41a8 -r d32c23d29968 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Mar 05 19:58:56 2016 +0100
+++ b/src/HOL/HOL.thy	Sat Mar 05 20:47:31 2016 +0100
@@ -105,6 +105,12 @@
 
 subsubsection \<open>Additional concrete syntax\<close>
 
+abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>" 10)
+  where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)"
+
+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)"
 
diff -r 6383440f41a8 -r d32c23d29968 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Sat Mar 05 19:58:56 2016 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Sat Mar 05 20:47:31 2016 +0100
@@ -20,11 +20,6 @@
   "_case_syntax":: "['a, cases_syn] => 'b"
   ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10)
 
-(* should become standard syntax once x-symbols supports it *)
-syntax (latex)
-  nexists :: "('a => bool) => bool"           (binder "\<nexists>" 10)
-translations
-  "\<nexists>x. P" <= "\<not>(\<exists>x. P)"
 
 (* SETS *)