src/HOL/Library/LaTeXsugar.thy

--- a/src/HOL/Library/LaTeXsugar.thy	Sun May 29 12:41:40 2005 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Mon May 30 08:21:58 2005 +0200
@@ -20,6 +20,12 @@
   "_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 *)
 
 (* empty set *)