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